Commit 2025-09-08 19:47 51b5bba0

View on Github →

feat(Analysis/SpecialFunctions): iterated derivative of cotangent (#27212)

Estimated changes

Modified Mathlib/Analysis/Complex/IntegerCompl.lean

added theorem Complex.upperHalfPlane_inter_integerComplement

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Cotangent.lean

modified theorem HasProdLocallyUniformlyOn_euler_sin_prod

modified theorem HasProdUniformlyOn_sineTerm_prod_on_compact

modified theorem Summable_cotTerm

added theorem cot_pi_mul_contDiffWithinAt

modified theorem cot_series_rep'

added theorem differentiableOn_iteratedDerivWithin_cotTerm

added theorem eqOn_iteratedDerivWithin_cotTerm_integerComplement

added theorem eqOn_iteratedDerivWithin_cotTerm_upperHalfPlaneSet

added theorem eqOn_iteratedDeriv_cotTerm

added theorem iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_div_pow

added theorem iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_zpow

added theorem iteratedDerivWithin_cot_sub_inv_eq_add_mul_tsum

modified theorem logDeriv_sin_div_eq_cot

modified theorem logDeriv_sineTerm_eq_cotTerm

modified theorem multipliableUniformlyOn_euler_sin_prod_on_compact

modified theorem multipliable_sineTerm

added theorem sin_pi_mul_ne_zero

deleted theorem sin_pi_z_ne_zero

added theorem summableLocallyUniformlyOn_iteratedDerivWithin_cotTerm

modified theorem tendsto_euler_sin_prod'

modified theorem tendsto_logDeriv_euler_cot_sub

modified theorem tendsto_logDeriv_euler_sin_div

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

added theorem EisensteinSeries.abs_norm_eq_max_natAbs

added theorem EisensteinSeries.abs_norm_eq_max_natAbs_neg