Commit 2025-12-27 18:03 f160a5e2

View on Github →

feat(NumberTheory/ModularForms/EisensteinSeries/Summable): add auxiliary E2 lemmas (#32955) This contains a series of lemmas that are needed in #32585 to prove how E2 transforms under the slash action.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Complex/IntegerCompl.lean

added theorem Complex.UpperHalfPlane.int_div_mem_integerComplement

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

added theorem UpperHalfPlane.im_pnat_div_pos

Modified Mathlib/NumberTheory/LSeries/RiemannZeta.lean

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

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

added theorem EisensteinSeries.isBigO_linear_add_const_vec

added theorem EisensteinSeries.isLittleO_const_left_of_properSpace_of_discreteTopology

added theorem EisensteinSeries.linear_inv_isBigO_right_add

deleted theorem EisensteinSeries.linear_isTheta_right

added theorem EisensteinSeries.linear_isTheta_right_add

added theorem EisensteinSeries.summable_linear_left_mul_linear_left

added theorem EisensteinSeries.summable_linear_right_add_one_mul_linear_right

added theorem EisensteinSeries.summable_of_isBigO_rpow_norm

added theorem EisensteinSeries.tendsto_zero_inv_linear

added theorem EisensteinSeries.tendsto_zero_inv_linear_sub

added theorem EisensteinSeries.vec_add_const_isTheta

Modified Mathlib/NumberTheory/ModularForms/Identities.lean

added theorem SlashInvariantForm.slash_S_apply

Created Mathlib/NumberTheory/TsumDivisorsAntidiagonal.lean

added def divisorsAntidiagonalFactors

added theorem divisorsAntidiagonalFactors_eq

added theorem divisorsAntidiagonalFactors_one

added def sigmaAntidiagonalEquivProd

added theorem sigmaAntidiagonalEquivProd_symm_apply_fst

added theorem sigmaAntidiagonalEquivProd_symm_apply_snd

added theorem summable_norm_pow_mul_geometric_div_one_sub

added theorem summable_prod_mul_pow

added theorem tendsto_zero_geometric_tsum_pnat

added theorem tsum_pow_div_one_sub_eq_tsum_sigma

added theorem tsum_prod_pow_eq_tsum_sigma

Modified Mathlib/NumberTheory/TsumDivsorsAntidiagonal.lean

deleted def divisorsAntidiagonalFactors

deleted theorem divisorsAntidiagonalFactors_eq

deleted theorem divisorsAntidiagonalFactors_one

deleted def sigmaAntidiagonalEquivProd

deleted theorem sigmaAntidiagonalEquivProd_symm_apply_fst

deleted theorem sigmaAntidiagonalEquivProd_symm_apply_snd

deleted theorem summable_norm_pow_mul_geometric_div_one_sub

deleted theorem summable_prod_mul_pow

deleted theorem tsum_pow_div_one_sub_eq_tsum_sigma

deleted theorem tsum_prod_pow_eq_tsum_sigma

Modified Mathlib/Order/Filter/AtTopBot/Archimedean.lean

added theorem tendsto_PNat_val_atTop_atTop

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

added theorem multipliable_pnat_iff_multipliable_nat

added theorem tprod_int_eq_zero_mul_tprod_pnat