Commit 2025-02-13 05:14 5dd13c2c

View on Github →

chore(MeasureTheory): process porting notes (#21787)

Estimated changes

Modified Mathlib/MeasureTheory/Constructions/Pi.lean

Modified Mathlib/MeasureTheory/Covering/VitaliFamily.lean

Modified Mathlib/MeasureTheory/Decomposition/Jordan.lean

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL2.lean

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.lean

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/Unique.lean

Modified Mathlib/MeasureTheory/Function/L1Space/Integrable.lean

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

Modified Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean

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

Modified Mathlib/MeasureTheory/Function/UnifTight.lean

Modified Mathlib/MeasureTheory/Function/UniformIntegrable.lean

Modified Mathlib/MeasureTheory/Integral/Average.lean

added theorem MeasureTheory.laverage_mul_measure_univ

Modified Mathlib/MeasureTheory/Integral/Bochner.lean

Modified Mathlib/MeasureTheory/Integral/BochnerL1.lean

modified theorem MeasureTheory.L1.integral_eq

Modified Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean

Modified Mathlib/MeasureTheory/Integral/IntervalIntegral.lean

Modified Mathlib/MeasureTheory/Integral/Layercake.lean

Modified Mathlib/MeasureTheory/Integral/Lebesgue.lean

Modified Mathlib/MeasureTheory/Integral/Prod.lean

Modified Mathlib/MeasureTheory/Integral/TorusIntegral.lean

Modified Mathlib/MeasureTheory/Integral/VitaliCaratheodory.lean

Modified Mathlib/MeasureTheory/Measure/Doubling.lean

Modified Mathlib/MeasureTheory/Measure/FiniteMeasure.lean

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

Modified Mathlib/MeasureTheory/Measure/Hausdorff.lean

Modified Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean

Modified Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean

Modified Mathlib/MeasureTheory/Measure/Typeclasses.lean

Modified Mathlib/MeasureTheory/OuterMeasure/AE.lean

Modified Mathlib/MeasureTheory/OuterMeasure/Induced.lean

Modified Mathlib/MeasureTheory/OuterMeasure/OfFunction.lean

Modified Mathlib/MeasureTheory/PiSystem.lean