isBoundedAt_iff_exists_SL2Z — Mathlib

English

Let c be a cusp and f: H → C, weight k. Then f is bounded at c iff there exists γ ∈ SL(2,Z) with γ•∞ = c such that f|[k]γ is bounded at ∞.

Русский

Пусть c — cusp и f: H → C, вес k. Тогда f ограничена в c тогда и только тогда, когда существует γ ∈ SL(2,Z) с γ•∞ = c, такое что f|[k]γ ограничена в ∞.

LaTeX

$$IsBoundedAt(c,f,k) ↔ ∃ γ ∈ SL(2,Z), (γ • ∞ = c) ∧ IsBoundedAtImInfty (f|[k] γ)$$

Lean4

theorem isBoundedAt_iff_exists_SL2Z (hc : IsCusp c 𝒮ℒ) :
    IsBoundedAt c f k ↔ ∃ γ : SL(2, ℤ), mapGL ℝ γ • ∞ = c ∧ IsBoundedAtImInfty (f ∣[k] γ) :=
  by
  constructor
  · obtain ⟨γ, rfl⟩ := isCusp_SL2Z_iff'.mp hc
    simpa [IsBoundedAt.smul_iff, isBoundedAt_infty_iff] using fun hfc ↦ ⟨γ, rfl, hfc⟩
  · rintro ⟨γ, rfl, b⟩
    simpa [IsBoundedAt.smul_iff, isBoundedAt_infty_iff] using b

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