English
Translation of a modular form by GL(2,ℝ) yields a new modular form of the same weight on the conjugated subgroup.
Русский
Перенос модульной формы по действию GL(2,ℝ) даёт новую модульную форму той же степени на сопряжённой подгруппе.
LaTeX
$$$\\text{Translate}_g: M_k(Γ) \\to M_k(g^{-1}Γg)$, and the translated form is defined by the slash action: $f|_k g$.$$
Lean4
/-- Translating a `ModularForm` by `GL(2, ℝ)`, to obtain a new `ModularForm`. -/
noncomputable def translate [ModularFormClass F Γ k] (g : GL (Fin 2) ℝ) : ModularForm (toConjAct g⁻¹ • Γ) k
where
__ := SlashInvariantForm.translate f g
bdd_at_cusps' {c} hc γ
hγ :=
by
rw [SlashInvariantForm.toFun_eq_coe, SlashInvariantForm.coe_translate, ← SlashAction.slash_mul, ←
isBoundedAt_infty_iff, ← OnePoint.IsBoundedAt.smul_iff]
apply ModularFormClass.bdd_at_cusps f
simpa [mul_smul, hγ] using hc.smul g
holo' := (ModularFormClass.holo f).slash k g
