Structures · Algebra
ModularFormClass
ModularFormClass F Γ k says that F is a type of bundled functions that extend
SlashInvariantFormClass by requiring that the functions be holomorphic and bounded
at all cusps.
- Defined in
- Mathlib.NumberTheory.ModularForms.Basic
- Shape
- 3 explicit arguments · adds holo, bdd_at_cusps
Extends1
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances1
- ModularForm
How is a type an instance?
Loading the hierarchy index…
Assumed by73
- ModularFormClass.analyticAt_cuspFunction_zero
- ModularForm.weakFEPair
- ModularFormClass.bdd_at_infty
- ModularFormClass.holo
- ModularForm.Λ
- ModularForm.translate
- ModularForm.norm
- ModularForm.qExpansion_smul
- ModularFormClass.modularForm
- ModularForm.L
- ModularFormClass.bdd_at_cusps
- ModularForm.qExpansion_sub
- ModularFormClass.continuous
- ModularForm.trace
- UpperHalfPlane.IsZeroAtImInfty.petersson_exp_decay_left
- ModularForm.qExpansion_mul_coe
- ModularFormClass.exp_decay_atImInfty'
- CuspFormClass.petersson_bounded_left
- ModularFormClass.levelOne_neg_weight_eq_zero
- qExpansion_coeff_isBigO_of_norm_isBigO
- ModularForm.coe_norm
- UpperHalfPlane.IsZeroAtImInfty.petersson_exp_decay_right
- ModularForm.weakFEPair_f
- ModularFormClass.bdd_at_infty_slash
- ModularForm.hasSum_Λ
- ModularFormClass.qExpansion_coeff_unique
- ModularFormClass.exists_bound
- ModularForm.cuspFunction_add
- ModularFormClass.levelOne_weight_zero_const
- ModularFormClass.qExpansion_isBigO
- ModularFormClass.exists_petersson_le
- ModularForm.cuspFunction_sub
- ModularForm.cuspFunction_neg
- UpperHalfPlane.IsZeroAtImInfty.petersson_isZeroAtImInfty_left
- ModularForm.isZeroAtImInfty_of_valueAtInfty_eq_zero
- ModularForm.weakFEPair_f₀
- ModularFormClass.qExpansion_coeff_eq_intervalIntegral
- ModularForm.qExpansion_neg
- ModularForm.norm_ne_zero
- ModularFormClass.exp_decay_sub_atImInfty'
- ModularForm.qExpansion_add
- ModularForm.cuspFunction_smul
- ModularForm.coe_translate
- ModularFormClass.qExpansion_smul
- ModularFormClass.qExpansion_add
- ModularForm.weakFEPair_k
- ModularForm.weakFEPair.congr_simp
- ModularForm.weakFEPair_ε
- ModularForm.norm_eq_zero_iff
- ModularForm.translate.congr_simp