Commit 2023-11-03 14:28 ab3030a0

View on Github →

feat: Fubini for functions with compact support and non-sigma-finite measures (#8125)

Estimated changes

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

added theorem MeasureTheory.integral_integral_swap_of_hasCompactSupport

Modified Mathlib/MeasureTheory/Function/SimpleFuncDense.lean

added theorem HasCompactSupport.exists_simpleFunc_approx_of_prod

added theorem HasCompactSupport.measurable_of_prod

Modified Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean

added theorem Continuous.stronglyMeasurable_of_hasCompactMulSupport

deleted theorem Continuous.stronglyMeasurable_of_hasCompactSupport

added theorem Continuous.stronglyMeasurable_of_mulSupport_subset_isCompact

added theorem HasCompactSupport.stronglyMeasurable_of_prod