Commit 2026-05-23 12:42 04f69b51

View on Github →

chore: cleanup Integral file (#39652)

Estimated changes

Modified Mathlib/MeasureTheory/Integral/Bochner/Basic.lean

modified theorem MeasureTheory.L1.integral_eq_integral

modified theorem MeasureTheory.SimpleFunc.integral_eq_integral

modified theorem MeasureTheory.SimpleFunc.integral_eq_sum

modified theorem MeasureTheory.integral_eq

modified theorem MeasureTheory.tendsto_integral_approxOn_of_measurable

modified theorem MeasureTheory.tendsto_integral_approxOn_of_measurable_of_range_subset

modified theorem MeasureTheory.tendsto_integral_of_L1'

modified theorem MeasureTheory.tendsto_integral_of_L1

modified theorem MeasureTheory.tendsto_setIntegral_of_L1'

modified theorem MeasureTheory.tendsto_setIntegral_of_L1

Modified Mathlib/MeasureTheory/Integral/DominatedConvergence.lean

Modified Mathlib/MeasureTheory/Integral/Prod.lean

Modified Mathlib/Probability/Kernel/Composition/IntegralCompProd.lean

Modified Mathlib/Probability/Kernel/Disintegration/Density.lean