Commit 2026-01-21 17:08 6c39be54

View on Github →

chore: move tsum lemmas in ENNReal.Lemmas to InfiniteSum.ENNReal (#34058) Many lemmas in Topology.Instances.ENNReal.Lemmas are about infinite sums, and belong rather to Topology.Algebra.InfiniteSum.ENNReal, so we move them here. Also Topology.Instances.ENNReal.Lemmas was becoming too long.

Estimated changes

added theorem ENNReal.hasSum_lt
added theorem ENNReal.hasSum_toReal
added theorem ENNReal.tsum_fiberwise
added theorem ENNReal.tsum_iSup_eq
added theorem ENNReal.tsum_iUnion_le
added theorem ENNReal.tsum_lt_tsum
added theorem ENNReal.tsum_sub
added theorem ENNReal.tsum_toReal_eq
added theorem ENNReal.tsum_union_le
added theorem NNReal.summable_of_le
added theorem NNReal.summable_sigma
added theorem NNReal.tsum_lt_tsum
added theorem NNReal.tsum_pos
added theorem Summable.toNNReal
deleted theorem ENNReal.hasProd_iInf_prod
deleted theorem ENNReal.hasSum_lt
deleted theorem ENNReal.hasSum_toReal
deleted theorem ENNReal.summable_toReal
deleted theorem ENNReal.tendsto_nat_tsum
deleted theorem ENNReal.tsum_biUnion_le
deleted theorem ENNReal.tsum_fiberwise
deleted theorem ENNReal.tsum_iSup_eq
deleted theorem ENNReal.tsum_iUnion_le
deleted theorem ENNReal.tsum_lt_tsum
deleted theorem ENNReal.tsum_mono_subtype
deleted theorem ENNReal.tsum_sub
deleted theorem ENNReal.tsum_toNNReal_eq
deleted theorem ENNReal.tsum_toReal_eq
deleted theorem ENNReal.tsum_union_le
deleted theorem NNReal.hasSum_strict_mono
deleted theorem NNReal.indicator_summable
deleted theorem NNReal.summable_of_le
deleted theorem NNReal.summable_sigma
deleted theorem NNReal.tsum_lt_tsum
deleted theorem NNReal.tsum_pos
deleted theorem NNReal.tsum_strict_mono
deleted theorem Summable.of_nonneg_of_le
deleted theorem Summable.toNNReal
deleted theorem tsum_comp_le_tsum_of_inj