Commit 2023-12-05 22:38 c6ea155e

View on Github →

feat: Binary products of finite measures and probability measures. (#8721) Upstreaming from PFR project This PR defines binary products of finite measures and probability measures.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Measure/FiniteMeasure.lean

modified theorem MeasureTheory.FiniteMeasure.map_apply

modified theorem MeasureTheory.FiniteMeasure.map_smul

added theorem MeasureTheory.FiniteMeasure.toMeasure_map

Created Mathlib/MeasureTheory/Measure/FiniteMeasureProd.lean

added theorem MeasureTheory.FiniteMeasure.map_fst_prod

added theorem MeasureTheory.FiniteMeasure.map_prod_map

added theorem MeasureTheory.FiniteMeasure.map_snd_prod

added theorem MeasureTheory.FiniteMeasure.mass_prod

added theorem MeasureTheory.FiniteMeasure.prod_apply

added theorem MeasureTheory.FiniteMeasure.prod_apply_symm

added theorem MeasureTheory.FiniteMeasure.prod_prod

added theorem MeasureTheory.FiniteMeasure.prod_swap

added theorem MeasureTheory.FiniteMeasure.prod_zero

added theorem MeasureTheory.FiniteMeasure.toMeasure_prod

added theorem MeasureTheory.FiniteMeasure.zero_prod

added theorem MeasureTheory.ProbabilityMeasure.map_fst_prod

added theorem MeasureTheory.ProbabilityMeasure.map_prod_map

added theorem MeasureTheory.ProbabilityMeasure.map_snd_prod

added theorem MeasureTheory.ProbabilityMeasure.prod_apply

added theorem MeasureTheory.ProbabilityMeasure.prod_apply_symm

added theorem MeasureTheory.ProbabilityMeasure.prod_prod

added theorem MeasureTheory.ProbabilityMeasure.prod_swap

added theorem MeasureTheory.ProbabilityMeasure.toMeasure_prod

Modified Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean

modified theorem MeasureTheory.ProbabilityMeasure.map_apply

added theorem MeasureTheory.ProbabilityMeasure.toMeasure_map