English
For z ∈ the upper half-plane and k ≥ 0, for every x : Fin 2 → ℤ, we have ‖x0 z + x1‖^(-k) ≤ (r z)^(-k) · ‖x‖^(-k).
Русский
Для z ∈ верхней полуплоскости и k ≥ 0, для каждого x ∈ ℤ^2 получаем неравенство ‖x0 z + x1‖^(-k) ≤ (r(z))^(-k) · ‖x‖^(-k).
LaTeX
$$$\\forall z \\in \\mathbb{H},\\; \\forall k \\in \\mathbb{R}_{\\ge 0},\\; \\forall x: \\mathbb{F}in 2 \\to \\mathbb{Z},\\; \\|x_0 z + x_1\\|^{-k} \\le (r(z))^{-k} \\|x\\|^{-k}$$$
Lean4
/-- Upper bound for the summand `|c * z + d| ^ (-k)`, as a product of a function of `z` and a
function of `c, d`. -/
theorem summand_bound {k : ℝ} (hk : 0 ≤ k) (x : Fin 2 → ℤ) : ‖x 0 * (z : ℂ) + x 1‖ ^ (-k) ≤ (r z) ^ (-k) * ‖x‖ ^ (-k) :=
by
by_cases hx : x = 0
· simp only [hx, Pi.zero_apply, Int.cast_zero, zero_mul, add_zero, norm_zero]
by_cases h : -k = 0
· rw [h, Real.rpow_zero, Real.rpow_zero, one_mul]
· rw [Real.zero_rpow h, mul_zero]
· rw [← Real.mul_rpow (r_pos _).le (norm_nonneg _)]
exact Real.rpow_le_rpow_of_nonpos (mul_pos (r_pos _) (norm_pos_iff.mpr hx)) (r_mul_max_le z hx) (neg_nonpos.mpr hk)
