Commit 2025-04-22 07:47 1ab4cd0a

View on Github →

chore(Measure): drop some assumptions (#23714) Add prod_apply_le/prod_prod_le and use them to drop SFinite _ assumptions here and there.

Estimated changes

Modified Mathlib/Analysis/Convolution.lean

Modified Mathlib/Analysis/Fourier/FourierTransform.lean

Modified Mathlib/MeasureTheory/Integral/Pi.lean

modified theorem MeasureTheory.Integrable.fin_nat_prod

modified theorem MeasureTheory.Integrable.fintype_prod

modified theorem MeasureTheory.Integrable.fintype_prod_dep

Modified Mathlib/MeasureTheory/Integral/Prod.lean

modified theorem MeasureTheory.AEStronglyMeasurable.fst

modified theorem MeasureTheory.AEStronglyMeasurable.snd

added theorem MeasureTheory.Integrable.mul_prod

added theorem MeasureTheory.Integrable.op_fst_snd

deleted theorem MeasureTheory.Integrable.prod_mul

deleted theorem MeasureTheory.Integrable.prod_smul

added theorem MeasureTheory.Integrable.smul_prod

Modified Mathlib/MeasureTheory/Measure/Prod.lean

modified theorem AEMeasurable.fst

modified theorem AEMeasurable.snd

added theorem MeasureTheory.Measure.measure_prod_null_of_ae_null

added theorem MeasureTheory.Measure.prod_apply_le

added theorem MeasureTheory.Measure.prod_prod_le

added theorem MeasureTheory.NullMeasurable.comp_fst

added theorem MeasureTheory.NullMeasurable.comp_snd

added theorem MeasureTheory.lintegral_prod_le

Modified Mathlib/MeasureTheory/Measure/QuasiMeasurePreserving.lean

added theorem MeasureTheory.NullMeasurable.comp_quasiMeasurePreserving