Commit 2024-11-16 20:53 2aeb1553

View on Github →

feat(NumberTheory/ModularForms): q-expansions of modular forms (#18813) Show that modular forms of level n can be written as analytic functions of q = exp (2 * pi * I * z / n).

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Complex/Periodic.lean

added theorem Function.Periodic.abs_qParam

added theorem Function.Periodic.abs_qParam_lt_iff

added theorem Function.Periodic.boundedAtFilter_cuspFunction

added def Function.Periodic.cuspFunction

added theorem Function.Periodic.cuspFunction_eq_of_nonzero

added theorem Function.Periodic.cuspFunction_zero_eq_limUnder_nhds_ne

added theorem Function.Periodic.cuspFunction_zero_of_zero_at_inf

added theorem Function.Periodic.differentiableAt_cuspFunction

added theorem Function.Periodic.differentiableAt_cuspFunction_zero

added theorem Function.Periodic.eq_cuspFunction

added theorem Function.Periodic.eventually_differentiableAt_cuspFunction_nhds_ne_zero

added theorem Function.Periodic.exp_decay_of_zero_at_inf

added theorem Function.Periodic.im_invQParam

added def Function.Periodic.invQParam

added theorem Function.Periodic.invQParam_tendsto

added def Function.Periodic.qParam

added theorem Function.Periodic.qParam_left_inv_mod_period

added theorem Function.Periodic.qParam_right_inv

added theorem Function.Periodic.qParam_tendsto

added theorem Function.Periodic.tendsto_at_I_inf

deleted theorem abs_qParam

deleted theorem abs_qParam_lt_iff

deleted theorem boundedAtFilter_cuspFunction

deleted def cuspFunction

deleted theorem cuspFunction_eq_of_nonzero

deleted theorem cuspFunction_zero_eq_limUnder_nhds_ne

deleted theorem cuspFunction_zero_of_zero_at_inf

deleted theorem differentiableAt_cuspFunction

deleted theorem differentiableAt_cuspFunction_zero

deleted theorem eq_cuspFunction

deleted theorem eventually_differentiableAt_cuspFunction_nhds_ne_zero

deleted theorem exp_decay_of_zero_at_inf

deleted theorem im_invQParam

deleted def invQParam

deleted theorem invQParam_tendsto

deleted def qParam

deleted theorem qParam_left_inv_mod_period

deleted theorem qParam_right_inv

deleted theorem qParam_tendsto

deleted theorem tendsto_at_I_inf

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

added theorem UpperHalfPlane.coe_mk_subtype

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

added theorem UpperHalfPlane.tendsto_coe_atImInfty

added theorem UpperHalfPlane.tendsto_comap_im_ofComplex

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

added theorem UpperHalfPlane.mdifferentiableAt_iff

added theorem UpperHalfPlane.mdifferentiableAt_ofComplex

added theorem UpperHalfPlane.mdifferentiable_iff

added theorem UpperHalfPlane.smoothAt_ofComplex

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

added theorem UpperHalfPlane.eventuallyEq_coe_comp_ofComplex

added theorem UpperHalfPlane.ofComplex_apply_of_im_pos

Created Mathlib/NumberTheory/ModularForms/QExpansion.lean

added theorem CuspFormClass.cuspFunction_apply_zero

added theorem CuspFormClass.exp_decay_atImInfty

added theorem CuspFormClass.zero_at_infty_comp_ofComplex

added theorem Function.Periodic.im_invQParam_pos_of_abs_lt_one

added theorem ModularFormClass.analyticAt_cuspFunction_zero

added theorem ModularFormClass.bounded_at_infty_comp_ofComplex

added theorem ModularFormClass.differentiableAt_comp_ofComplex

added theorem ModularFormClass.differentiableAt_cuspFunction

added def SlashInvariantFormClass.cuspFunction

added theorem SlashInvariantFormClass.eq_cuspFunction

added theorem SlashInvariantFormClass.periodic_comp_ofComplex