English
If z ∈ 𝒟ᵒ and g•z ∈ 𝒟ᵒ, then |g_{1,0}| ≤ 1.
Русский
Пусть z ∈ 𝒟ᵒ и g•z ∈ 𝒟ᵒ; тогда |g_{1,0}| ≤ 1.
LaTeX
$$$ z\in 𝒟^{\circ} \land (g\cdot z)\in 𝒟^{\circ} \Rightarrow |g_{1,0}| \le 1$$$
Lean4
/-- An auxiliary result en route to `ModularGroup.c_eq_zero`. -/
theorem abs_c_le_one (hz : z ∈ 𝒟ᵒ) (hg : g • z ∈ 𝒟ᵒ) : |g 1 0| ≤ 1 :=
by
let c' : ℤ := g 1 0
let c := (c' : ℝ)
suffices 3 * c ^ 2 < 4
by
rw [← Int.cast_pow, ← Int.cast_three, ← Int.cast_four, ← Int.cast_mul, Int.cast_lt] at this
replace this : c' ^ 2 ≤ 1 ^ 2 := by omega
rwa [sq_le_sq, abs_one] at this
suffices c ≠ 0 → 9 * c ^ 4 < 16 by
rcases eq_or_ne c 0 with (hc | hc)
· rw [hc]; simp
· refine (abs_lt_of_sq_lt_sq' ?_ (by simp)).2
specialize this hc
linarith
intro hc
have h₁ : 3 * 3 * c ^ 4 < 4 * (g • z).im ^ 2 * (4 * z.im ^ 2) * c ^ 4 := by
gcongr <;> apply three_lt_four_mul_im_sq_of_mem_fdo <;> assumption
have h₂ : (c * z.im) ^ 4 / normSq (denom (↑g) z) ^ 2 ≤ 1 :=
div_le_one_of_le₀ (pow_four_le_pow_two_of_pow_two_le (z.c_mul_im_sq_le_normSq_denom g)) (sq_nonneg _)
let nsq := normSq (denom g z)
calc
9 * c ^ 4 < c ^ 4 * z.im ^ 2 * (g • z).im ^ 2 * 16 := by linarith
_ = c ^ 4 * z.im ^ 4 / nsq ^ 2 * 16 := by
rw [im_smul_eq_div_normSq, div_pow]
ring
_ ≤ 16 := by rw [← mul_pow]; linarith
