normSq_div_sub_div_lt_one — Mathlib

English

See item 153788 for a closely related bound on the difference between x/y and its Gaussian-integer approximation.

Русский

См. пункт 153788 для близкого по смыслу ограничения на разность x/y и его гауссовой целой аппроксимации.

LaTeX

$$$ \text{(same as normSq_div_sub_div_lt_one)} $$$

Lean4

theorem normSq_div_sub_div_lt_one (x y : ℤ[i]) : Complex.normSq ((x / y : ℂ) - ((x / y : ℤ[i]) : ℂ)) < 1 :=
  calc
    Complex.normSq ((x / y : ℂ) - ((x / y : ℤ[i]) : ℂ))
    _ =
        Complex.normSq
          ((x / y : ℂ).re - ((x / y : ℤ[i]) : ℂ).re + ((x / y : ℂ).im - ((x / y : ℤ[i]) : ℂ).im) * I : ℂ) :=
      (congr_arg _ <| by apply Complex.ext <;> simp)
    _ ≤ Complex.normSq (1 / 2 + 1 / 2 * I) :=
      by
      have : |(2⁻¹ : ℝ)| = 2⁻¹ := abs_of_nonneg (by simp)
      exact
        normSq_le_normSq_of_re_le_of_im_le
          (by rw [toComplex_re_div]; simp [normSq, this]; simpa using abs_sub_round (x / y : ℂ).re)
          (by rw [toComplex_im_div]; simp [normSq, this]; simpa using abs_sub_round (x / y : ℂ).im)
    _ < 1 := by simp [normSq]; norm_num

Похожие утверждения