English
For z ∈ the upper half-plane and x ∈ ℤ^2 not both zero, r(z)·‖x‖ ≤ ‖x0 z + x1‖.
Русский
Для z в верхней полуплоскости и x ∈ ℤ^2 не равного нулю, выполняется r(z)·‖x‖ ≤ ‖x0 z + x1‖.
LaTeX
$$$\\forall z \\in \\mathbb{H},\\; \\forall x:\\, \\mathbb{F}in 2 \\to \\mathbb{Z},\\; x \\neq 0 \\Rightarrow r(z) \\cdot \\|x\\| \\le \\| x_0 z + x_1 \\|$$$
Lean4
theorem r_mul_max_le {x : Fin 2 → ℤ} (hx : x ≠ 0) : r z * ‖x‖ ≤ ‖x 0 * (z : ℂ) + x 1‖ :=
by
have hn0 : ‖x‖ ≠ 0 := by rwa [norm_ne_zero_iff]
have h11 : x 0 * (z : ℂ) + x 1 = (x 0 / ‖x‖ * z + x 1 / ‖x‖) * ‖x‖ := by
rw [div_mul_eq_mul_div, ← add_div, div_mul_cancel₀ _ (mod_cast hn0)]
rw [norm_eq_max_natAbs, h11, norm_mul, norm_real, norm_norm, norm_eq_max_natAbs]
gcongr
· rcases div_max_sq_ge_one x hx with H1 | H2
· simpa only [norm_eq_max_natAbs, ofReal_div, ofReal_intCast] using auxbound1 z (x 1 / ‖x‖) H1
· simpa only [norm_eq_max_natAbs, ofReal_div, ofReal_intCast] using auxbound2 z (x 0 / ‖x‖) H2
