bdd_at_infty_slash — Mathlib

English

Translating a cusp form by SL(2,Z) gives a cusp form for the SL(2,Z)-modified group.

Русский

Перенос cusp-формы по SL(2,Z) образует cusp-форму для группы, модифицированной SL(2,Z).

LaTeX

$$$[\\text{CuspFormClass} F Γ k] \\to [\\text{CuspForm}(Γ')]$, $Γ' = (toConjAct)^{-1} · Γ$ with $g\\in SL(2,\\mathbb{Z})$.$$

Lean4

theorem bdd_at_infty_slash [ModularFormClass F Γ k] (f : F) (g : SL(2, ℤ)) : IsBoundedAtImInfty (f ∣[k] g) :=
  by
  rw [← OnePoint.isBoundedAt_infty_iff, SL_slash, ← OnePoint.IsBoundedAt.smul_iff]
  apply bdd_at_cusps f
  rw [Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z, isCusp_SL2Z_iff']
  exact ⟨g, by simp [mapGL]⟩

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