Commit 2024-02-27 15:33 740f664f
View on Github →feat(MeasureTheory/Integral): hasSum_integral_of_summable_integral_norm (#10614)
A lemma on interchanging sums and integrals (pretty much equivalent tointegral_tsum, but without explicitly mentioning ENNReals, lintegrals etc). Also, correct a random capitalisation glitch I spotted in the process.