Commit 2026-01-07 13:28 772b00fb

View on Github →

feat(Analysis): ℘ is analytic (#32911)

Estimated changes

Modified Mathlib/Analysis/Analytic/Binomial.lean

deleted theorem Real.hasFPowerSeriesOnBall_linear_zero

added theorem Real.hasFPowerSeriesOnBall_ofScalars_mul_add_zero

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

added theorem PeriodPair.PeriodPairs.analyticOnNhd_derivWeierstrassP

added theorem PeriodPair.analyticOnNhd_derivWeierstrassPExcept

added theorem PeriodPair.analyticOnNhd_weierstrassP

added theorem PeriodPair.analyticOnNhd_weierstrassPExcept

added theorem PeriodPair.coeff_weierstrassPExceptSeries

added theorem PeriodPair.coeff_weierstrassPSeries

added def PeriodPair.derivWeierstrassPExceptSeries

added theorem PeriodPair.hasFPowerSeriesOnBall_derivWeierstrassPExcept

added theorem PeriodPair.hasFPowerSeriesOnBall_weierstrassP

added theorem PeriodPair.hasFPowerSeriesOnBall_weierstrassPExcept

added theorem PeriodPair.hasSum_sumInvPow

added theorem PeriodPair.ite_eq_one_sub_sq_mul_weierstrassP

added theorem PeriodPair.meromorphic_weierstrassP

added theorem PeriodPair.order_weierstrassP

added def PeriodPair.sumInvPow

added theorem PeriodPair.summable_weierstrassPExceptSummand

added theorem PeriodPair.summable_weierstrassPSummand

added def PeriodPair.weierstrassPExceptSeries

added theorem PeriodPair.weierstrassPExceptSeries_hasSum

added theorem PeriodPair.weierstrassPExceptSeries_of_notMem

added def PeriodPair.weierstrassPExceptSummand

added theorem PeriodPair.weierstrassPExceptSummand_of_notMem

added theorem PeriodPair.weierstrassPExcept_eq_tsum

added def PeriodPair.weierstrassPSeries

added theorem PeriodPair.weierstrassPSeries_hasSum

added def PeriodPair.weierstrassPSummand

Modified Mathlib/Order/UpperLower/Closure.lean

added theorem lowerClosure_eq_top

added theorem lowerClosure_eq_top_iff

added theorem upperClosure_eq_bot

added theorem upperClosure_eq_bot_iff

Modified Mathlib/Topology/Order/IsLUB.lean

added theorem lowerClosure_eq_Iic_csSup

added theorem upperClosure_eq_Ici_csInf