English
As a simp lemma, the constant real-valued modular form evaluates to its real value embedded in ℂ.
Русский
Как вспомогательная лемма при упрощении, постоянная вещественная модульная форма оценивается в своей вещественной величине, встроенной в ℂ.
LaTeX
$$$ (\mathrm{const}_{\mathbb{R}}(x))(\tau) = x \in \mathbb{C}. $$$
Lean4
/-- The constant function with value `x : ℂ` as a modular form of weight 0 and any level. -/
def constℝ (x : ℝ) [Γ.HasDetPlusMinusOne] : ModularForm Γ 0
where
toSlashInvariantForm := .constℝ x
holo' _ := mdifferentiableAt_const
bdd_at_cusps' hc g
hg := by
simpa only [constℝ_toFun, slash_def, SlashInvariantForm.toFun_eq_coe, Function.const_apply, neg_zero,
zpow_zero] using atImInfty.const_boundedAtFilter _
