Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-24 12:24 563f8c4f

View on Github →

feat(measure_theory/integral): dominated convergence for a series (#10398)

Estimated changes

Modified src/measure_theory/integral/bochner.lean

added theorem measure_theory.has_sum_integral_of_dominated_convergence

Modified src/measure_theory/integral/interval_integral.lean

added theorem interval_integral.has_sum_integral_of_dominated_convergence

added theorem interval_integral.tendsto_integral_filter_of_dominated_convergence