Commit 2024-06-12 13:30 a0732879

View on Github →

chore: split Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (#13756)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Calculus/FDeriv/Measurable.lean

Modified Mathlib/MeasureTheory/Function/AEEqFun/DomAct.lean

Modified Mathlib/MeasureTheory/Function/L1Space.lean

Modified Mathlib/MeasureTheory/Function/LpSpace.lean

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

deleted theorem ContinuousLinearMap.aestronglyMeasurable_comp₂

deleted theorem MeasureTheory.AEStronglyMeasurable.apply_continuousLinearMap

deleted theorem MeasureTheory.AEStronglyMeasurable.comp_measurePreserving

deleted theorem MeasureTheory.MeasurePreserving.aestronglyMeasurable_comp_iff

deleted theorem StronglyMeasurable.apply_continuousLinearMap

deleted theorem aestronglyMeasurable_smul_const_iff

deleted theorem aestronglyMeasurable_withDensity_iff

Created Mathlib/MeasureTheory/Function/StronglyMeasurable/Lemmas.lean

added theorem ContinuousLinearMap.aestronglyMeasurable_comp₂

added theorem MeasureTheory.AEStronglyMeasurable.apply_continuousLinearMap

added theorem MeasureTheory.AEStronglyMeasurable.comp_measurePreserving

added theorem MeasureTheory.MeasurePreserving.aestronglyMeasurable_comp_iff

added theorem StronglyMeasurable.apply_continuousLinearMap

added theorem aestronglyMeasurable_smul_const_iff

added theorem aestronglyMeasurable_withDensity_iff

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

Modified test/measurability.lean