English
For coprime bottom row p, the absolute value of the real part of g•z tends to infinity as g ranges over SL(2,ℤ) with bottom row p.
Русский
Для взаимно простой нижней строки p абсциссной части g•z стремится к бесконечности при обходе g в SL(2,ℤ) с нижней строкой p.
LaTeX
$$$\\forall p\\in \\mathbb{Z}^2,\\; \\gcd(p_0,p_1)=1:\\; Tendsto\\bigl(g\\mapsto |\\Re(g\\cdot z)|\\bigr)\\; \\text{коэффициентный к }\\; \\infty.$$$
Lean4
theorem tendsto_abs_re_smul {p : Fin 2 → ℤ} (hp : IsCoprime (p 0) (p 1)) :
Tendsto (fun g : { g : SL(2, ℤ) // g 1 = p } => |((g : SL(2, ℤ)) • z).re|) cofinite atTop :=
by
suffices Tendsto (fun g : (fun g : SL(2, ℤ) => g 1) ⁻¹' { p } => ((g : SL(2, ℤ)) • z).re) cofinite (cocompact ℝ) by
exact tendsto_norm_cocompact_atTop.comp this
have : ((p 0 : ℝ) ^ 2 + (p 1 : ℝ) ^ 2)⁻¹ ≠ 0 := by
apply inv_ne_zero
exact mod_cast hp.sq_add_sq_ne_zero
let f := Homeomorph.mulRight₀ _ this
let ff := Homeomorph.addRight (((p 1 : ℂ) * z - p 0) / (((p 0 : ℂ) ^ 2 + (p 1 : ℂ) ^ 2) * (p 0 * z + p 1))).re
convert (f.trans ff).isClosedEmbedding.tendsto_cocompact.comp (tendsto_lcRow0 hp) with _ _ g
change
((g : SL(2, ℤ)) • z).re =
lcRow0 p ↑(↑g : SL(2, ℝ)) / ((p 0 : ℝ) ^ 2 + (p 1 : ℝ) ^ 2) +
Complex.re (((p 1 : ℂ) * z - p 0) / (((p 0 : ℂ) ^ 2 + (p 1 : ℂ) ^ 2) * (p 0 * z + p 1)))
exact mod_cast congr_arg Complex.re (smul_eq_lcRow0_add z hp g.2)
