Commit 2026-05-26 07:57 31748419

View on Github →

chore: drop completeness from the definition of conditional expectation (#39862) This is not interesting from a mathematical point of view (in all reasonable applications, the spaces are complete), but it is a direct byproduct of the change to setToFun in #39615, and it means that whenever we write conditional expectations the job of Lean is easier (as it doesn't have to look for completeness) and the resulting term is simpler.

Estimated changes

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

modified theorem MeasureTheory.condExp_ae_eq_condExpL1

modified theorem MeasureTheory.condExp_ae_eq_condExpL1CLM

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

modified def MeasureTheory.condExpL1

modified def MeasureTheory.condExpL1CLM

modified theorem MeasureTheory.condExpL1_congr_ae

modified theorem MeasureTheory.condExpL1_eq

modified theorem MeasureTheory.condExpL1_of_aestronglyMeasurable'

modified theorem MeasureTheory.setIntegral_condExpL1

Modified Mathlib/Probability/Martingale/Basic.lean

modified theorem MeasureTheory.Martingale.eq_zero_of_predictable'

modified theorem MeasureTheory.Martingale.eq_zero_of_predictable

modified theorem MeasureTheory.Submartingale.sum_smul_sub

modified theorem MeasureTheory.Supermartingale.sub_martingale

modified theorem MeasureTheory.Supermartingale.sub_submartingale

modified theorem MeasureTheory.martingale_condExp

modified theorem MeasureTheory.martingale_iff

modified theorem MeasureTheory.martingale_nat

modified theorem MeasureTheory.martingale_of_condExp_sub_eq_zero_nat

modified theorem MeasureTheory.martingale_of_setIntegral_eq_succ

Modified Mathlib/Probability/Martingale/Centering.lean

modified theorem MeasureTheory.Martingale.martingalePart_eq

modified theorem MeasureTheory.Martingale.predictablePart_eq_zero

modified theorem MeasureTheory.Submartingale.monotone_predictablePart

modified theorem MeasureTheory.Submartingale.predictablePart_nonneg

modified theorem MeasureTheory.integrable_martingalePart

modified theorem MeasureTheory.martingalePart_add

modified theorem MeasureTheory.martingalePart_add_ae_eq

modified theorem MeasureTheory.martingalePart_smul

modified theorem MeasureTheory.martingale_martingalePart

modified theorem MeasureTheory.predictablePart_add

modified theorem MeasureTheory.predictablePart_add_ae_eq

modified theorem MeasureTheory.predictablePart_smul