isBoundedAt_iff_forall_SL2Z — Mathlib

English

For a cusp c, function f, and weight k, f is bounded at c iff for every γ ∈ SL(2,Z) with γ•∞ = c, the transformed function f|[k] γ is bounded at ∞.

Русский

Для вершины c, функции f и веса 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_forall_SL2Z (hc : IsCusp c 𝒮ℒ) :
    IsBoundedAt c f k ↔ ∀ γ : SL(2, ℤ), mapGL ℝ γ • ∞ = c → IsBoundedAtImInfty (f ∣[k] γ) :=
  by
  refine ⟨fun hc _ hγ ↦ by simpa using hc _ hγ, fun h ↦ ?_⟩
  obtain ⟨γ, rfl⟩ := isCusp_SL2Z_iff'.mp hc
  simpa [IsBoundedAt.smul_iff, isBoundedAt_infty_iff] using h γ rfl

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