Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-17 12:16 4afd667f

View on Github →

feat(measure_theory/integral): add integral_sum_measure (#12090) Also add supporting lemmas about finite and infinite sums of measures.

Estimated changes

Modified src/measure_theory/function/l1_space.lean

deleted theorem integrable_zero_measure

added theorem measure_theory.integrable_finset_sum_measure

added theorem measure_theory.integrable_zero_measure

Modified src/measure_theory/group/fundamental_domain.lean

added theorem measure_theory.is_fundamental_domain.pairwise_ae_disjoint_of_ac

Modified src/measure_theory/integral/bochner.lean

added theorem measure_theory.has_sum_integral_measure

added theorem measure_theory.integral_finset_sum_measure

added theorem measure_theory.integral_sum_measure

added theorem measure_theory.nndist_integral_add_measure_le_lintegral

Modified src/measure_theory/integral/lebesgue.lean

added theorem measure_theory.has_sum_lintegral_measure

added theorem measure_theory.lintegral_finset_sum_measure

Modified src/measure_theory/integral/set_integral.lean

added theorem measure_theory.has_sum_integral_Union_ae

deleted theorem measure_theory.has_sum_integral_Union_of_null_inter

added theorem measure_theory.integral_Union_ae

deleted theorem measure_theory.integral_Union_of_null_inter

Modified src/measure_theory/measure/measure_space.lean

added def measure_theory.measure.coe_add_hom

added theorem measure_theory.measure.coe_finset_sum

added theorem measure_theory.measure.finset_sum_apply

added theorem measure_theory.measure.sum_add_sum_compl

added theorem measure_theory.measure.sum_coe_finset

added theorem measure_theory.measure.sum_fintype