Commit 2025-08-25 12:07 c3ce1816

View on Github →

feat(NumberTheory/ModularForms): the Dedekind Eta function (#28400) We define the Dedekind eta function in preparation for later relating it to Eisenstein series and the modular form Delta.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Complex/Periodic.lean

added theorem Function.Periodic.contDiff_qParam

added theorem Function.Periodic.differentiable_qParam

added theorem Function.Periodic.qParam_ne_zero

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

added theorem UpperHalfPlane.isOpen_upperHalfPlaneSet

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

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

Modified Mathlib/Analysis/SpecialFunctions/Log/Summable.lean

added theorem Summable.summable_log_norm_one_add

added theorem tprod_one_add_ne_zero_of_summable

Modified Mathlib/NumberTheory/ModularForms/Basic.lean

Created Mathlib/NumberTheory/ModularForms/DedekindEta.lean

added theorem ModularForm.differentiableAt_eta_of_mem_upperHalfPlaneSet

added theorem ModularForm.eta_ne_zero

added theorem ModularForm.eta_q_eq_cexp

added theorem ModularForm.eta_q_eq_pow

added theorem ModularForm.logDeriv_one_sub_cexp

added theorem ModularForm.logDeriv_one_sub_mul_cexp_comp

added theorem ModularForm.multipliableLocallyUniformlyOn_eta

added theorem ModularForm.one_sub_eta_q_ne_zero

added theorem ModularForm.summable_eta_q

added theorem ModularForm.tsum_logDeriv_eta_q

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