one_lt_normSq_T_zpow_smul — Mathlib

English

For every z ∈ 𝒟ᵒ and every n ∈ ℤ, we have 1 < normSq (T^n • z).

Русский

Для каждого z ∈ 𝒟ᵒ и каждого n ∈ ℤ выполняется 1 < normSq (T^n • z).

LaTeX

$$$\forall z\in 𝒟^{\circ}, \forall n\in \mathbb{Z}, 1 < \operatorname{normSq}(T^{n} \cdot z)$$$

Lean4

/-- If `z ∈ 𝒟ᵒ`, and `n : ℤ`, then `|z + n| > 1`. -/
theorem one_lt_normSq_T_zpow_smul (hz : z ∈ 𝒟ᵒ) (n : ℤ) : 1 < normSq (T ^ n • z : ℍ) :=
  by
  rw [coe_T_zpow_smul_eq]
  have hz₁ : 1 < z.re * z.re + z.im * z.im := hz.1
  have hzn := Int.nneg_mul_add_sq_of_abs_le_one n (abs_two_mul_re_lt_one_of_mem_fdo hz).le
  have : 1 < (z.re + ↑n) * (z.re + ↑n) + z.im * z.im := by linarith
  simpa [normSq, num, denom]

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