three_le_four_mul_im_sq_of_mem_fd

English

If τ belongs to the open standard fundamental domain 𝒟ᵒ, then 3 ≤ 4 · (Im τ)^2.

Русский

Пусть τ принадлежит открытой стандартной фундаментальной области 𝒟ᵒ, тогда 3 ≤ 4 · (Imag τ)^2.

LaTeX

$$$\forall \tau \in 𝒟,\; 3 \le 4\, (\operatorname{Im}\tau)^2$$$

Lean4

/-- non-strict variant of `ModularGroup.three_le_four_mul_im_sq_of_mem_fdo` -/
theorem three_le_four_mul_im_sq_of_mem_fd {τ : ℍ} (h : τ ∈ 𝒟) : 3 ≤ 4 * τ.im ^ 2 :=
  by
  have : 1 ≤ τ.re * τ.re + τ.im * τ.im := by simpa [Complex.normSq_apply] using h.1
  cases abs_cases τ.re <;> nlinarith [h.2]

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