Commit 2023-12-01 08:27 7f904e5f

View on Github →

feat: extend results on product measures from sigma-finite to s-finite measures (#8713)

Estimated changes

Modified Mathlib/Analysis/Calculus/Rademacher.lean

Modified Mathlib/Logic/Function/Basic.lean

deleted theorem Function.FactorsThrough.apply_extend

deleted theorem Function.Injective.apply_extend

added theorem Function.apply_extend

Modified Mathlib/MeasureTheory/Constructions/Pi.lean

Modified Mathlib/MeasureTheory/Constructions/Prod/Basic.lean

modified theorem AEMeasurable.fst

modified theorem AEMeasurable.prod_swap

modified theorem AEMeasurable.snd

modified theorem Measurable.lintegral_prod_left'

modified theorem Measurable.lintegral_prod_left

modified theorem Measurable.lintegral_prod_right'

modified theorem Measurable.lintegral_prod_right

modified theorem Measurable.map_prod_mk_left

modified theorem Measurable.map_prod_mk_right

modified theorem MeasureTheory.Measure.AbsolutelyContinuous.prod

modified theorem MeasureTheory.Measure.add_prod

modified theorem MeasureTheory.Measure.map_prod_map

modified theorem MeasureTheory.Measure.prodAssoc_prod

modified theorem MeasureTheory.Measure.prod_add

modified theorem MeasureTheory.Measure.prod_eq

modified theorem MeasureTheory.Measure.prod_sum

added theorem MeasureTheory.Measure.prod_sum_left

added theorem MeasureTheory.Measure.prod_sum_right

deleted theorem MeasureTheory.Measure.sum_prod

modified theorem MeasureTheory.MeasurePreserving.skew_product

modified theorem MeasureTheory.lintegral_lintegral_swap

modified theorem MeasureTheory.lintegral_lintegral_symm

modified theorem MeasureTheory.lintegral_prod_swap

modified theorem MeasureTheory.lintegral_prod_symm'

modified theorem MeasureTheory.lintegral_prod_symm

modified theorem measurable_measure_prod_mk_left

modified theorem measurable_measure_prod_mk_right

Modified Mathlib/MeasureTheory/Group/Measure.lean

Modified Mathlib/MeasureTheory/Measure/AEMeasurable.lean

added theorem MeasureTheory.Measure.map_sum

Modified Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

modified theorem MeasureTheory.Measure.sum_add_sum

modified theorem MeasureTheory.Measure.sum_apply

added theorem MeasureTheory.Measure.sum_apply_of_countable

added theorem MeasureTheory.Measure.sum_comp_equiv

added theorem MeasureTheory.Measure.sum_extend_zero

added theorem MeasureTheory.Measure.sum_sum

Modified Mathlib/MeasureTheory/Measure/Restrict.lean

added theorem MeasureTheory.Measure.restrict_sum_of_countable

Modified Mathlib/MeasureTheory/Measure/Typeclasses.lean

added theorem MeasureTheory.sfinite_sum_of_countable

Modified Mathlib/Topology/Algebra/InfiniteSum/Basic.lean

added theorem tsum_extend_zero