Commit 2026-02-05 18:04 4b5dfe66

View on Github →

feat(NumberTheory/ModularForms/DedekindEta): Show logDeriv eta is E2 (#34217) We prove that up to a constant, the logarithmic derivative of the Dedekind eta functions is the Eisenstein series E2. This comes from work done for the Sphere Packing project.

Estimated changes

Modified Mathlib/Analysis/Calculus/LogDeriv.lean

modified theorem logDeriv_prod

Modified Mathlib/Analysis/Calculus/LogDerivUniformlyOn.lean

modified theorem logDeriv_tprod_eq_tsum

Modified Mathlib/Analysis/Complex/LocallyUniformLimit.lean

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Cotangent.lean

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean

deleted theorem Complex.LogDeriv_exp

added theorem Complex.logDeriv_exp

deleted theorem Real.LogDeriv_exp

added theorem Real.logDeriv_exp

Modified Mathlib/NumberTheory/ModularForms/DedekindEta.lean

added theorem ModularForm.differentiableAt_eta_tprod

modified theorem ModularForm.eta_ne_zero

added theorem ModularForm.eta_tprod_ne_zero

added theorem ModularForm.logDeriv_eta_eq_E2

added theorem ModularForm.logDeriv_qParam

added theorem ModularForm.summable_logDeriv_one_sub_eta_q