Commit 2024-05-27 14:30 3efcf495

View on Github →

Eisenstein series are mdifferentiable (#11013) We show that Eisenstein Series are MDifferentiable

depends on: #10377
depends on: #11244

Estimated changes

Modified Mathlib.lean

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

added theorem UpperHalfPlane.comp_ofComplex

added def UpperHalfPlane.ofComplex

added theorem UpperHalfPlane.ofComplex_apply

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

added theorem EisensteinSeries.div_linear_zpow_differentiableOn

added theorem EisensteinSeries.eisSummand_extension_differentiableOn

added theorem EisensteinSeries.eisensteinSeries_SIF_MDifferentiable

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