Commit 2025-01-22 16:34 4ccc2ce0

View on Github →

feat: make Integrable provable by fun_prop (#20952)

Estimated changes

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

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

Modified Mathlib/MeasureTheory/Function/L1Space.lean

added theorem MeasureTheory.Integrable.add''

added theorem MeasureTheory.Integrable.sub'

Modified Mathlib/MeasureTheory/Function/L2Space.lean

Modified Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean

Modified Mathlib/MeasureTheory/Integral/IntegrableOn.lean

Modified Mathlib/Probability/Distributions/Gaussian.lean

Modified Mathlib/Probability/Martingale/Centering.lean

Modified Mathlib/Probability/Moments/Basic.lean

Modified Mathlib/Probability/Moments/IntegrableExpMul.lean

Modified Mathlib/Probability/Variance.lean