Commit 2026-03-06 23:58 6e9770b3

View on Github →

feat(ModularForm/NumberTheory/Delta): Define the delta function (#34881) We define the Delta function on the upper half plane and show how it transforms under the slash operator, this is in preparation to proving it is a modular form.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Complex/SqrtDeriv.lean

added theorem Complex.continuousAt_sqrt

added theorem Complex.continuousOn_sqrt

added theorem Complex.derivWithin_sqrt

added theorem Complex.deriv_sqrt

added theorem Complex.differentiableAt_sqrt

added theorem Complex.differentiableOn_sqrt

added theorem Complex.differentiableWithinAt_sqrt

added theorem Complex.hasDerivAt_sqrt

added theorem Complex.hasDerivWithinAt_sqrt

added theorem Complex.hasStrictDerivAt_sqrt

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

added theorem UpperHalfPlane.mem_slitPlane

Modified Mathlib/Analysis/RCLike/Sqrt.lean

added theorem sqrt_eq_exp

Created Mathlib/NumberTheory/ModularForms/Delta.lean

added theorem ModularForm.csqrt_I_pow_24

added theorem ModularForm.csqrt_pow_24_eq

added theorem ModularForm.delta_S_invariant

added theorem ModularForm.delta_T_invariant

added theorem ModularForm.delta_eq_q_prod

added theorem ModularForm.delta_ne_zero

added theorem ModularForm.eta_comp_eqOn_const_mul_csqrt_eta

added theorem ModularForm.eta_comp_eq_csqrt_I_inv

added theorem ModularForm.logDeriv_eta_comp_div_eq

added theorem ModularForm.logDeriv_eta_comp_eq_logDeriv_csqrt_eta

Modified Mathlib/Topology/Algebra/InfiniteSum/Basic.lean

added theorem HasProd.pow

added theorem Multipliable.pow

added theorem Multipliable.tprod_pow