English
For every τ ∈ ℍ, there exists γ ∈ SL(2,ℤ) with im(γ•τ) ≥ 1/2 and ‖denom γ τ‖ ≤ 1.
Русский
Для любого τ ∈ ℍ существует γ ∈ SL(2,ℤ) такое, что im(γ•τ) ≥ 1/2 и ‖denom γ τ‖ ≤ 1.
LaTeX
$$$\forall \tau\in ℍ, \exists \gamma\in SL(2,ℤ), \tfrac{1}{2} \le \operatorname{im}(\gamma\cdot \tau) \land \|\operatorname{denom}(\gamma) \tau\| \le 1$$$
Lean4
/-- For every `τ : ℍ` there is some `γ ∈ SL(2, ℤ)` that sends it to an element whose
imaginary part is at least `1/2` and such that `denom γ τ` has norm at most 1. -/
theorem exists_one_half_le_im_smul_and_norm_denom_le (τ : ℍ) : ∃ γ : SL(2, ℤ), 1 / 2 ≤ im (γ • τ) ∧ ‖denom γ τ‖ ≤ 1 :=
by
rcases le_total (1 / 2) τ.im with h | h
· exact ⟨1, (one_smul SL(2, ℤ) τ).symm ▸ h, by simp only [map_one, denom_one, norm_one, le_refl]⟩
· refine (exists_one_half_le_im_smul τ).imp (fun γ hγ ↦ ⟨hγ, ?_⟩)
have h1 : τ.im ≤ (γ • τ).im := h.trans hγ
rw [im_smul_eq_div_normSq, le_div_iff₀ (normSq_denom_pos γ τ.im_ne_zero), normSq_eq_norm_sq] at h1
simpa only [sq_le_one_iff_abs_le_one, abs_norm] using (mul_le_iff_le_one_right τ.2).mp h1
