Commit 2023-05-29 08:45 cd203c8f

View on Github →

feat: port MeasureTheory.Constructions.Prod.Basic (#4433)

Estimated changes

Modified Mathlib.lean

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

added theorem AEMeasurable.fst

added theorem AEMeasurable.prod_swap

added theorem AEMeasurable.snd

added theorem IsCountablySpanning.prod

added theorem IsPiSystem.prod

added theorem Measurable.lintegral_prod_left'

added theorem Measurable.lintegral_prod_left

added theorem Measurable.lintegral_prod_right'

added theorem Measurable.lintegral_prod_right

added theorem Measurable.map_prod_mk_left

added theorem Measurable.map_prod_mk_right

added theorem MeasurableEmbedding.prod_mk

added theorem MeasureTheory.Measure.AbsolutelyContinuous.prod

added theorem MeasureTheory.Measure.add_prod

added theorem MeasureTheory.Measure.ae_ae_of_ae_prod

added theorem MeasureTheory.Measure.ae_measure_lt_top

added theorem MeasureTheory.Measure.dirac_prod

added theorem MeasureTheory.Measure.dirac_prod_dirac

added theorem MeasureTheory.Measure.fst_apply

added theorem MeasureTheory.Measure.fst_univ

added theorem MeasureTheory.Measure.map_prod_map

added theorem MeasureTheory.Measure.measurePreserving_swap

added theorem MeasureTheory.Measure.measure_ae_null_of_prod_null

added theorem MeasureTheory.Measure.measure_prod_null

added theorem MeasureTheory.Measure.prodAssoc_prod

added theorem MeasureTheory.Measure.prod_add

added theorem MeasureTheory.Measure.prod_apply

added theorem MeasureTheory.Measure.prod_apply_symm

added theorem MeasureTheory.Measure.prod_dirac

added theorem MeasureTheory.Measure.prod_eq

added theorem MeasureTheory.Measure.prod_eq_generateFrom

added theorem MeasureTheory.Measure.prod_prod

added theorem MeasureTheory.Measure.prod_restrict

added theorem MeasureTheory.Measure.prod_sum

added theorem MeasureTheory.Measure.prod_swap

added theorem MeasureTheory.Measure.prod_zero

added theorem MeasureTheory.Measure.quasiMeasurePreserving_fst

added theorem MeasureTheory.Measure.quasiMeasurePreserving_snd

added theorem MeasureTheory.Measure.restrict_prod_eq_prod_univ

added theorem MeasureTheory.Measure.snd_apply

added theorem MeasureTheory.Measure.snd_univ

added theorem MeasureTheory.Measure.sum_prod

added theorem MeasureTheory.Measure.volume_eq_prod

added theorem MeasureTheory.Measure.zero_prod

added theorem MeasureTheory.MeasurePreserving.skew_product

added theorem MeasureTheory.QuasiMeasurePreserving.prod_of_left

added theorem MeasureTheory.QuasiMeasurePreserving.prod_of_right

added theorem MeasureTheory.lintegral_lintegral

added theorem MeasureTheory.lintegral_lintegral_swap

added theorem MeasureTheory.lintegral_lintegral_symm

added theorem MeasureTheory.lintegral_prod

added theorem MeasureTheory.lintegral_prod_mul

added theorem MeasureTheory.lintegral_prod_of_measurable

added theorem MeasureTheory.lintegral_prod_swap

added theorem MeasureTheory.lintegral_prod_symm'

added theorem MeasureTheory.lintegral_prod_symm

added theorem generateFrom_eq_prod

added theorem generateFrom_prod

added theorem generateFrom_prod_eq

added theorem isPiSystem_prod

added theorem measurable_measure_prod_mk_left

added theorem measurable_measure_prod_mk_left_finite

added theorem measurable_measure_prod_mk_right