Commit 2026-04-23 17:52 63a91877

View on Github →

feat(NumberTheory/ModularForms/QExpansion): update qExpansion API for more general objects (#36474) This PR generalises several lemmas from ModularFormClass and ModularForm to functions on the upper half plane that are periodic, holomorphic, and bounded at infinity. This allows us to study the q-expansion of functions such as q * j, where j denotes the j-function. The specialised ModularFormClass and ModularForm lemmas are retained as wrappers.

Estimated changes

Modified Mathlib/NumberTheory/ModularForms/Bounds.lean

Modified Mathlib/NumberTheory/ModularForms/EisensteinSeries/QExpansion.lean

Modified Mathlib/NumberTheory/ModularForms/LevelOne.lean

Modified Mathlib/NumberTheory/ModularForms/Petersson.lean

Modified Mathlib/NumberTheory/ModularForms/QExpansion.lean

deleted theorem CuspFormClass.cuspFunction_apply_zero

deleted theorem CuspFormClass.exp_decay_atImInfty'

deleted theorem CuspFormClass.exp_decay_atImInfty

deleted theorem CuspFormClass.zero_at_infty_comp_ofComplex

deleted theorem ModularFormClass.analyticAt_cuspFunction_zero

deleted theorem ModularFormClass.cuspFunction_apply_zero

deleted theorem ModularFormClass.differentiableAt_comp_ofComplex

deleted theorem ModularFormClass.differentiableAt_cuspFunction

deleted theorem ModularFormClass.differentiableOn_cuspFunction_ball

deleted theorem ModularFormClass.exp_decay_sub_atImInfty'

deleted theorem ModularFormClass.exp_decay_sub_atImInfty

deleted theorem ModularFormClass.hasFPowerSeries_cuspFunction

deleted theorem ModularFormClass.hasSum_qExpansion

deleted theorem ModularFormClass.hasSum_qExpansion_of_norm_lt

deleted def ModularFormClass.qExpansion

deleted def ModularFormClass.qExpansionFormalMultilinearSeries

deleted theorem ModularFormClass.qExpansionFormalMultilinearSeries_apply_norm

deleted theorem ModularFormClass.qExpansionFormalMultilinearSeries_coeff

deleted theorem ModularFormClass.qExpansionFormalMultilinearSeries_radius

deleted theorem ModularFormClass.qExpansion_coeff

deleted theorem ModularFormClass.qExpansion_coeff_eq_circleIntegral

deleted theorem ModularFormClass.qExpansion_coeff_eq_intervalIntegral

deleted theorem ModularFormClass.qExpansion_coeff_zero

deleted def SlashInvariantFormClass.cuspFunction

deleted theorem SlashInvariantFormClass.eq_cuspFunction

added theorem UpperHalfPlane.IsZeroAtImInfty.CuspFormClass.cuspFunction_apply_zero

added theorem UpperHalfPlane.IsZeroAtImInfty.CuspFormClass.exp_decay_atImInfty'

added theorem UpperHalfPlane.IsZeroAtImInfty.CuspFormClass.exp_decay_atImInfty

added theorem UpperHalfPlane.IsZeroAtImInfty.CuspFormClass.zero_at_infty_comp_ofComplex

added def UpperHalfPlane.IsZeroAtImInfty.ModularForm.qExpansionAddHom

added def UpperHalfPlane.IsZeroAtImInfty.ModularForm.qExpansionRingHom

added theorem UpperHalfPlane.IsZeroAtImInfty.ModularForm.qExpansionRingHom_apply

added theorem UpperHalfPlane.IsZeroAtImInfty.ModularForm.qExpansion_of_mul

added theorem UpperHalfPlane.IsZeroAtImInfty.ModularForm.qExpansion_of_pow

added theorem UpperHalfPlane.IsZeroAtImInfty.ModularFormClass.exp_decay_atImInfty'

added theorem UpperHalfPlane.IsZeroAtImInfty.ModularFormClass.exp_decay_sub_atImInfty'

added theorem UpperHalfPlane.IsZeroAtImInfty.UpperHalfPlane.cuspFunction_add

added theorem UpperHalfPlane.IsZeroAtImInfty.UpperHalfPlane.cuspFunction_mul

added theorem UpperHalfPlane.IsZeroAtImInfty.UpperHalfPlane.cuspFunction_mul_zero

added theorem UpperHalfPlane.IsZeroAtImInfty.UpperHalfPlane.cuspFunction_neg

added theorem UpperHalfPlane.IsZeroAtImInfty.UpperHalfPlane.cuspFunction_smul

added theorem UpperHalfPlane.IsZeroAtImInfty.UpperHalfPlane.cuspFunction_sub

added theorem UpperHalfPlane.IsZeroAtImInfty.UpperHalfPlane.hasFPowerSeries_cuspFunction

added theorem UpperHalfPlane.IsZeroAtImInfty.UpperHalfPlane.qExpansion_add

added theorem UpperHalfPlane.IsZeroAtImInfty.UpperHalfPlane.qExpansion_coeff_unique

added theorem UpperHalfPlane.IsZeroAtImInfty.UpperHalfPlane.qExpansion_eq_zero_iff

added theorem UpperHalfPlane.IsZeroAtImInfty.UpperHalfPlane.qExpansion_mul

added theorem UpperHalfPlane.IsZeroAtImInfty.UpperHalfPlane.qExpansion_mul_coeff_zero

added theorem UpperHalfPlane.IsZeroAtImInfty.UpperHalfPlane.qExpansion_neg

added theorem UpperHalfPlane.IsZeroAtImInfty.UpperHalfPlane.qExpansion_one

added theorem UpperHalfPlane.IsZeroAtImInfty.UpperHalfPlane.qExpansion_smul

added theorem UpperHalfPlane.IsZeroAtImInfty.UpperHalfPlane.qExpansion_sub

added theorem UpperHalfPlane.IsZeroAtImInfty.UpperHalfPlane.qExpansion_zero

deleted theorem UpperHalfPlane.IsZeroAtImInfty.exp_decay_atImInfty'

modified theorem UpperHalfPlane.IsZeroAtImInfty.exp_decay_atImInfty

added theorem UpperHalfPlane.analyticAt_cuspFunction_zero

added def UpperHalfPlane.cuspFunction

added theorem UpperHalfPlane.cuspFunction_apply_zero

added theorem UpperHalfPlane.differentiableAt_cuspFunction

added theorem UpperHalfPlane.differentiableOn_cuspFunction_ball

added theorem UpperHalfPlane.eq_cuspFunction

added theorem UpperHalfPlane.exp_decay_sub_atImInfty

added theorem UpperHalfPlane.hasFPowerSeriesOnBall_cuspFunction

added theorem UpperHalfPlane.hasSum_qExpansion

added theorem UpperHalfPlane.hasSum_qExpansion_of_norm_lt

added def UpperHalfPlane.qExpansion

added def UpperHalfPlane.qExpansionFormalMultilinearSeries

added theorem UpperHalfPlane.qExpansionFormalMultilinearSeries_apply_norm

added theorem UpperHalfPlane.qExpansionFormalMultilinearSeries_coeff

added theorem UpperHalfPlane.qExpansionFormalMultilinearSeries_radius

added theorem UpperHalfPlane.qExpansion_coeff

added theorem UpperHalfPlane.qExpansion_coeff_eq_circleIntegral

added theorem UpperHalfPlane.qExpansion_coeff_eq_intervalIntegral

added theorem UpperHalfPlane.qExpansion_coeff_zero

deleted theorem cuspFunction_add

deleted theorem cuspFunction_mul

deleted theorem cuspFunction_mul_zero

deleted theorem cuspFunction_neg

deleted theorem cuspFunction_smul

deleted theorem cuspFunction_sub

deleted theorem hasFPowerSeriesOnBall_cuspFunction

deleted def qExpansionAddHom

deleted def qExpansionRingHom

deleted theorem qExpansionRingHom_apply

deleted theorem qExpansion_add

deleted theorem qExpansion_coeff_unique

deleted theorem qExpansion_eq_zero_iff

deleted theorem qExpansion_mul

deleted theorem qExpansion_mul_coeff_zero

deleted theorem qExpansion_neg

deleted theorem qExpansion_of_mul

deleted theorem qExpansion_of_pow

deleted theorem qExpansion_one

deleted theorem qExpansion_smul

deleted theorem qExpansion_sub

deleted theorem qExpansion_zero