Commit 2024-07-08 13:05 d4585053

View on Github →

Eisenstein series are bounded at infinity (#12456) We show the IsBoundedAtImInfty property for Eisenstein series.

Estimated changes

Modified Mathlib.lean

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

modified def EisensteinSeries.eisSummand

added theorem EisensteinSeries.eisensteinSeries_SIF_apply

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

added theorem EisensteinSeries.abs_le_tsum_abs

added theorem EisensteinSeries.isBoundedAtImInfty_eisensteinSeries_SIF

added theorem EisensteinSeries.summable_norm_eisSummand

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