Commit 2023-02-24 18:18 733fa004

View on Github →

feat(measure_theory/integral): integration lemmas from #18392 (#18466) Some lemmas about integration of continuous functions split off from my Poisson-summation / zeta-functions project at #18392.

Estimated changes

Modified src/measure_theory/integral/interval_integral.lean

added theorem interval_integral.has_sum_interval_integral_of_summable_norm

added theorem interval_integral.tsum_interval_integral_eq_of_summable_norm

Modified src/measure_theory/integral/set_integral.lean

added theorem measure_theory.integrable_of_summable_norm_restrict

modified theorem measure_theory.integrable_on_Union_of_summable_integral_norm

added theorem measure_theory.integrable_on_Union_of_summable_norm_restrict

Modified src/measure_theory/measure/lebesgue.lean

added theorem real.integrable_of_summable_norm_Icc