Commit 2026-10-27 21:33 7ed8b096

View on Github →

feat(Topology/Algebra/InfiniteSum): Deprecate generalized ENNReal lemmas (#38193) Following the PR #38489, this PR add deprecated tags to the original ENNReal lemmas and change the transitive children files to use the generalized lemmas rather than the deprecated lemmas. Related Zulip thread: #Is there code for X? > Summing ENats without topology

Estimated changes

Modified Mathlib/Analysis/Normed/Group/InfiniteSum.lean

Modified Mathlib/Analysis/PSeries.lean

Modified Mathlib/Analysis/SpecificLimits/Basic.lean

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean

Modified Mathlib/MeasureTheory/Covering/Besicovitch.lean

Modified Mathlib/MeasureTheory/Covering/Differentiation.lean

Modified Mathlib/MeasureTheory/Covering/Vitali.lean

Modified Mathlib/MeasureTheory/Function/AEMeasurableOrder.lean

Modified Mathlib/MeasureTheory/Function/BorelGrowth.lean

Modified Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean

Modified Mathlib/MeasureTheory/Function/Egorov.lean

Modified Mathlib/MeasureTheory/Function/Jacobian.lean

Modified Mathlib/MeasureTheory/Function/LpSpace/Complete.lean

Modified Mathlib/MeasureTheory/Function/LpSpace/InfiniteSum.lean

Modified Mathlib/MeasureTheory/Function/SimpleFunc.lean

Modified Mathlib/MeasureTheory/Integral/Bochner/VitaliCaratheodory.lean

Modified Mathlib/MeasureTheory/Integral/Lebesgue/Add.lean

Modified Mathlib/MeasureTheory/Integral/Lebesgue/Basic.lean

Modified Mathlib/MeasureTheory/Integral/Lebesgue/Countable.lean

Modified Mathlib/MeasureTheory/Measure/AbsolutelyContinuous.lean

Modified Mathlib/MeasureTheory/Measure/AddContent.lean

Modified Mathlib/MeasureTheory/Measure/Basic.lean

Modified Mathlib/MeasureTheory/Measure/CompleteLattice.lean

Modified Mathlib/MeasureTheory/Measure/Content.lean

Modified Mathlib/MeasureTheory/Measure/Continuity.lean

Modified Mathlib/MeasureTheory/Measure/Count.lean

Modified Mathlib/MeasureTheory/Measure/Hausdorff.lean

Modified Mathlib/MeasureTheory/Measure/MeasuredSets.lean

Modified Mathlib/MeasureTheory/Measure/Module.lean

Modified Mathlib/MeasureTheory/Measure/MutuallySingular.lean

Modified Mathlib/MeasureTheory/Measure/PreVariation.lean

Modified Mathlib/MeasureTheory/Measure/Prokhorov.lean

Modified Mathlib/MeasureTheory/Measure/Regular.lean

Modified Mathlib/MeasureTheory/Measure/RegularityCompacts.lean

Modified Mathlib/MeasureTheory/Measure/Restrict.lean

Modified Mathlib/MeasureTheory/Measure/Stieltjes.lean

Modified Mathlib/MeasureTheory/Measure/Sum.lean

Modified Mathlib/MeasureTheory/Measure/Typeclasses/SFinite.lean

Modified Mathlib/MeasureTheory/Measure/WithDensity.lean

Modified Mathlib/MeasureTheory/OuterMeasure/Caratheodory.lean

Modified Mathlib/MeasureTheory/OuterMeasure/Induced.lean

Modified Mathlib/MeasureTheory/OuterMeasure/OfAddContent.lean

Modified Mathlib/MeasureTheory/OuterMeasure/OfFunction.lean

Modified Mathlib/MeasureTheory/OuterMeasure/Operations.lean

Modified Mathlib/MeasureTheory/VectorMeasure/Operations.lean

Modified Mathlib/NumberTheory/Transcendental/Liouville/Measure.lean

Modified Mathlib/Probability/Kernel/Defs.lean

Modified Mathlib/Probability/Kernel/WithDensity.lean

Modified Mathlib/Probability/ProbabilityMassFunction/Basic.lean

Modified Mathlib/Probability/ProbabilityMassFunction/Constructions.lean

Modified Mathlib/Probability/ProbabilityMassFunction/Monad.lean

Modified Mathlib/Probability/Process/LocalProperty.lean

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

deleted theorem ENNReal.tsum_biUnion_le

deleted theorem ENNReal.tsum_biUnion_le_tsum

deleted theorem ENNReal.tsum_comp_le_tsum_of_injective

deleted theorem ENNReal.tsum_eq_add_tsum_ite

deleted theorem ENNReal.tsum_fiberwise

deleted theorem ENNReal.tsum_iUnion_le

deleted theorem ENNReal.tsum_iUnion_le_tsum

deleted theorem ENNReal.tsum_le_tsum_comp_of_surjective

deleted theorem ENNReal.tsum_mono_subtype

deleted theorem ENNReal.tsum_union_le

modified theorem Summable.countable_support_ennreal

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

modified theorem CompleteLattice.summable

Modified Mathlib/Topology/MetricSpace/PiNat.lean

Modified Mathlib/Topology/Semicontinuity/Basic.lean