Commit 2026-03-18 13:09 41280ad9

View on Github →

feat(ModularForms): (normalized) derivative of modular forms (#36405) Derivative of modular forms, stems from Sphere Packing project. The major goal is two-fold: prove Ramanujan's identities and also prove that Serre derivative preserves modularity (first uses second).

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/ModularForms/Derivative.lean

added def Derivative.normalizedDerivOfComplex

added theorem Derivative.normalizedDerivOfComplex_add

added theorem Derivative.normalizedDerivOfComplex_const

added theorem Derivative.normalizedDerivOfComplex_mdifferentiable

added theorem Derivative.normalizedDerivOfComplex_mul

added theorem Derivative.normalizedDerivOfComplex_neg

added theorem Derivative.normalizedDerivOfComplex_pow

added theorem Derivative.normalizedDerivOfComplex_smul

added theorem Derivative.normalizedDerivOfComplex_sub

added def Derivative.serreDerivative

added theorem Derivative.serreDerivative_add

added theorem Derivative.serreDerivative_apply

added theorem Derivative.serreDerivative_eq

added theorem Derivative.serreDerivative_mdifferentiable

added theorem Derivative.serreDerivative_mul

added theorem Derivative.serreDerivative_smul

added theorem Derivative.serreDerivative_sub