Commit 2025-12-04 09:22 d94916e1

View on Github →

feat(NumberTheory/ModularForms): improvements to q-expansions (#32060) Generalize q-expansion theory so it works for any discrete subgroup of GL2R, and express the q-expansion coefficients as integrals (using the Cauchy integral formula for derivatives)

Estimated changes

Modified Mathlib/Analysis/Complex/Periodic.lean

added theorem Function.Periodic.exp_decay_sub_of_bounded_at_inf

Modified Mathlib/Analysis/Complex/UpperHalfPlane/FunctionsBoundedAtInfty.lean

Modified Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean

added theorem isLittleO_exp_mul_rpow_of_lt

Modified Mathlib/NumberTheory/ModularForms/Basic.lean

modified theorem CuspFormClass.zero_at_infty

modified theorem CuspFormClass.zero_at_infty_slash

modified theorem ModularFormClass.bdd_at_infty

modified theorem ModularFormClass.bdd_at_infty_slash

modified theorem ModularFormClass.continuous

Modified Mathlib/NumberTheory/ModularForms/Cusps.lean

added theorem Subgroup.isCusp_of_mem_strictPeriods

Modified Mathlib/NumberTheory/ModularForms/Identities.lean

added theorem SlashInvariantForm.vAdd_apply_of_mem_strictPeriods

Modified Mathlib/NumberTheory/ModularForms/LevelOne.lean

added theorem ModularFormClass.one_mem_strictPeriods_SL2Z

Modified Mathlib/NumberTheory/ModularForms/Petersson.lean

added theorem SlashInvariantFormClass.norm_petersson_smul

added theorem UpperHalfPlane.IsZeroAtImInfty.of_exp_decay

added theorem UpperHalfPlane.IsZeroAtImInfty.petersson_exp_decay_left

added theorem UpperHalfPlane.IsZeroAtImInfty.petersson_exp_decay_right

added theorem UpperHalfPlane.IsZeroAtImInfty.petersson_isZeroAtImInfty_left

added theorem UpperHalfPlane.IsZeroAtImInfty.petersson_isZeroAtImInfty_right

added theorem UpperHalfPlane.petersson_norm_symm

added theorem UpperHalfPlane.petersson_symm

Modified Mathlib/NumberTheory/ModularForms/QExpansion.lean

modified theorem CuspFormClass.cuspFunction_apply_zero

added theorem CuspFormClass.exp_decay_atImInfty'

modified theorem CuspFormClass.exp_decay_atImInfty

modified theorem CuspFormClass.zero_at_infty_comp_ofComplex

modified theorem ModularFormClass.analyticAt_cuspFunction_zero

modified theorem ModularFormClass.bounded_at_infty_comp_ofComplex

added theorem ModularFormClass.cuspFunction_apply_zero

modified theorem ModularFormClass.differentiableAt_cuspFunction

added theorem ModularFormClass.differentiableOn_cuspFunction_ball

added theorem ModularFormClass.exp_decay_sub_atImInfty'

added theorem ModularFormClass.exp_decay_sub_atImInfty

modified theorem ModularFormClass.hasFPowerSeries_cuspFunction

modified theorem ModularFormClass.hasSum_qExpansion

deleted theorem ModularFormClass.hasSum_qExpansion_of_abs_lt

added theorem ModularFormClass.hasSum_qExpansion_of_norm_lt

modified theorem ModularFormClass.qExpansionFormalMultilinearSeries_radius

added theorem ModularFormClass.qExpansion_coeff_eq_circleIntegral

added theorem ModularFormClass.qExpansion_coeff_eq_intervalIntegral

added theorem ModularFormClass.qExpansion_coeff_zero

modified def SlashInvariantFormClass.cuspFunction

modified theorem SlashInvariantFormClass.eq_cuspFunction

modified theorem SlashInvariantFormClass.periodic_comp_ofComplex

added theorem UpperHalfPlane.IsZeroAtImInfty.cuspFunction_apply_zero

added theorem UpperHalfPlane.IsZeroAtImInfty.exp_decay_atImInfty'

added theorem UpperHalfPlane.IsZeroAtImInfty.exp_decay_atImInfty

added theorem UpperHalfPlane.IsZeroAtImInfty.valueAtInfty_eq_zero

added theorem UpperHalfPlane.IsZeroAtImInfty.zero_at_infty_comp_ofComplex

added theorem UpperHalfPlane.qParam_tendsto_atImInfty

added def UpperHalfPlane.valueAtInfty