Commit 2023-06-06 14:40 892102ca

View on Github →

feat: port MeasureTheory.Constructions.Prod.Integral (#4727)

Estimated changes

Modified Mathlib.lean

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

added theorem MeasureTheory.AEStronglyMeasurable.fst

added theorem MeasureTheory.AEStronglyMeasurable.integral_prod_right'

added theorem MeasureTheory.AEStronglyMeasurable.prod_mk_left

added theorem MeasureTheory.AEStronglyMeasurable.snd

added theorem MeasureTheory.Integrable.integral_norm_prod_left

added theorem MeasureTheory.Integrable.integral_norm_prod_right

added theorem MeasureTheory.Integrable.integral_prod_left

added theorem MeasureTheory.Integrable.integral_prod_right

added theorem MeasureTheory.Integrable.prod_left_ae

added theorem MeasureTheory.Integrable.prod_right_ae

added theorem MeasureTheory.Integrable.swap

added theorem MeasureTheory.Measure.integrable_measure_prod_mk_left

added theorem MeasureTheory.StronglyMeasurable.integral_prod_left'

added theorem MeasureTheory.StronglyMeasurable.integral_prod_left

added theorem MeasureTheory.StronglyMeasurable.integral_prod_right'

added theorem MeasureTheory.StronglyMeasurable.integral_prod_right

added theorem MeasureTheory.continuous_integral_integral

added theorem MeasureTheory.hasFiniteIntegral_prod_iff'

added theorem MeasureTheory.hasFiniteIntegral_prod_iff

added theorem MeasureTheory.integrable_prod_iff'

added theorem MeasureTheory.integrable_prod_iff

added theorem MeasureTheory.integrable_prod_mul

added theorem MeasureTheory.integrable_swap_iff

added theorem MeasureTheory.integral_fn_integral_add

added theorem MeasureTheory.integral_fn_integral_sub

added theorem MeasureTheory.integral_integral

added theorem MeasureTheory.integral_integral_add'

added theorem MeasureTheory.integral_integral_add

added theorem MeasureTheory.integral_integral_sub'

added theorem MeasureTheory.integral_integral_sub

added theorem MeasureTheory.integral_integral_swap

added theorem MeasureTheory.integral_integral_symm

added theorem MeasureTheory.integral_prod

added theorem MeasureTheory.integral_prod_mul

added theorem MeasureTheory.integral_prod_swap

added theorem MeasureTheory.integral_prod_symm

added theorem MeasureTheory.lintegral_fn_integral_sub

added theorem MeasureTheory.set_integral_prod

added theorem MeasureTheory.set_integral_prod_mul

added theorem measurableSet_integrable

Modified Mathlib/MeasureTheory/Function/LpSpace.lean