Commit 2024-07-11 14:18 33d2c7a1

View on Github →

feat(MeasureTheory): weaken assumptions from SigmaFinite to SFinite (#14638)

Weaken TC assumptions of many lemmas from SigmaFinite to SFinite.
Drop some MeasurableSet assumptions.

Estimated changes

Modified Mathlib/Analysis/Convolution.lean

modified theorem BddAbove.convolutionExistsAt

modified theorem MeasureTheory.convolution_congr

modified theorem MeasureTheory.integrable_posConvolution

modified theorem MeasureTheory.integral_posConvolution

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

modified theorem MeasureTheory.AEStronglyMeasurable.fst

modified theorem MeasureTheory.AEStronglyMeasurable.integral_prod_right'

modified theorem MeasureTheory.AEStronglyMeasurable.prod_mk_left

modified theorem MeasureTheory.AEStronglyMeasurable.snd

modified theorem MeasureTheory.Integrable.integral_norm_prod_right

modified theorem MeasureTheory.Integrable.integral_prod_right

modified theorem MeasureTheory.Integrable.prod_left_ae

modified theorem MeasureTheory.Integrable.prod_right_ae

modified theorem MeasureTheory.Integrable.swap

modified theorem MeasureTheory.StronglyMeasurable.integral_prod_left'

modified theorem MeasureTheory.StronglyMeasurable.integral_prod_left

modified theorem MeasureTheory.StronglyMeasurable.integral_prod_right'

modified theorem MeasureTheory.StronglyMeasurable.integral_prod_right

modified theorem MeasureTheory.integrable_prod_iff'

modified theorem MeasureTheory.integrable_swap_iff

modified theorem measurableSet_integrable

Modified Mathlib/MeasureTheory/Group/Prod.lean

modified theorem MeasureTheory.ae_measure_preimage_mul_right_lt_top

modified theorem MeasureTheory.ae_measure_preimage_mul_right_lt_top_of_ne_zero

modified theorem MeasureTheory.measure_eq_div_smul

modified theorem MeasureTheory.measure_lintegral_div_measure

modified theorem MeasureTheory.measure_mul_measure_eq

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

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