im_lt_im_S_smul — Mathlib

English

If z lies in the open fundamental domain 𝒟°, then Im(z) < Im(S•z).

Русский

Если z лежит в открытом фундаментальном домене 𝒟°, тогда Im(z) < Im(S•z).

LaTeX

$$$\\forall z \\in 𝒟^{\\circ},\\; \\Im(z) < \\Im(S\\cdot z).$$$

Lean4

/-- If `|z| < 1`, then applying `S` strictly decreases `im`. -/
theorem im_lt_im_S_smul (h : normSq z < 1) : z.im < (S • z).im :=
  by
  rw [ModularGroup.im_smul_eq_div_normSq]
  have : z.im < z.im / normSq (z : ℂ) := by
    have imz : 0 < z.im := im_pos z
    apply (lt_div_iff₀ z.normSq_pos).mpr
    nlinarith
  simpa [denom, coe_S, SpecialLinearGroup.toGL]

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