Commit 2025-12-05 11:03 ce933310

View on Github →

feat(Analysis): derivative of Weierstrass ℘ (#32089)

Estimated changes

Modified Mathlib/Analysis/SpecialFunctions/Elliptic/Weierstrass.lean

added def PeriodPair.derivWeierstrassP

added def PeriodPair.derivWeierstrassPExcept

added theorem PeriodPair.derivWeierstrassPExcept_add_coe

added theorem PeriodPair.derivWeierstrassPExcept_def

added theorem PeriodPair.derivWeierstrassPExcept_neg

added theorem PeriodPair.derivWeierstrassPExcept_of_notMem

added theorem PeriodPair.derivWeierstrassPExcept_sub

added theorem PeriodPair.derivWeierstrassP_add_coe

added theorem PeriodPair.derivWeierstrassP_coe

added theorem PeriodPair.derivWeierstrassP_neg

added theorem PeriodPair.derivWeierstrassP_sub_coe

added theorem PeriodPair.derivWeierstrassP_zero

added theorem PeriodPair.deriv_weierstrassP

added theorem PeriodPair.differentiableOn_derivWeierstrassP

added theorem PeriodPair.differentiableOn_derivWeierstrassPExcept

added theorem PeriodPair.eqOn_deriv_weierstrassPExcept_derivWeierstrassPExcept

added theorem PeriodPair.hasSumLocallyUniformly_derivWeierstrassP

added theorem PeriodPair.hasSumLocallyUniformly_derivWeierstrassPExcept

added theorem PeriodPair.hasSum_derivWeierstrassP

added theorem PeriodPair.hasSum_derivWeierstrassPExcept

added theorem PeriodPair.isOpen_compl_lattice_diff

added theorem PeriodPair.not_continuousAt_weierstrassP

added theorem PeriodPair.periodic_derivWeierstrassP

added theorem PeriodPair.periodic_weierstrassP

added theorem PeriodPair.weierstrassP_add_coe

added theorem PeriodPair.weierstrassP_coe

added theorem PeriodPair.weierstrassP_sub_coe

added theorem PeriodPair.weierstrassP_zero