English
For every z ∈ ℍ there exists g ∈ SL(2,ℤ) that maximizes the imaginary part among all SL(2,ℤ) translates of z.
Русский
Для каждого z ∈ ℍ существует g ∈ SL(2,ℤ), который максимизирует мнимую часть при всем трансляциям z действием SL(2,ℤ).
LaTeX
$$$\\forall z\\in \\mathbb{H},\\; \\exists g\\in SL(2,\\mathbb{Z}),\\; \\forall g'\\in SL(2,\\mathbb{Z}),\\; (g'\\cdot z)_{\\Im} \\le (g\\cdot z)_{\\Im}.$$$
Lean4
/-- For `z : ℍ`, there is a `g : SL(2,ℤ)` maximizing `(g•z).im` -/
theorem exists_max_im : ∃ g : SL(2, ℤ), ∀ g' : SL(2, ℤ), (g' • z).im ≤ (g • z).im := by
classical
let s : Set (Fin 2 → ℤ) := {cd | IsCoprime (cd 0) (cd 1)}
have hs : s.Nonempty := ⟨![1, 1], isCoprime_one_left⟩
obtain ⟨p, hp_coprime, hp⟩ := Filter.Tendsto.exists_within_forall_le hs (tendsto_normSq_coprime_pair z)
obtain ⟨g, -, hg⟩ := bottom_row_surj hp_coprime
refine ⟨g, fun g' => ?_⟩
rw [ModularGroup.im_smul_eq_div_normSq, ModularGroup.im_smul_eq_div_normSq, div_le_div_iff_of_pos_left]
· simpa [← hg] using hp (g' 1) (bottom_row_coprime g')
· exact z.im_pos
· exact normSq_denom_pos g' z.im_ne_zero
· exact normSq_denom_pos g z.im_ne_zero
