Commit 2025-12-04 19:47 1ff540cc

View on Github →

feat: generalize the codomain in Martingale.Basic (#31439) Many lemmas in Martingale.Basic are stated for real-valued process. If the results are about martingales, we generalize to real Banach spaces. If the results are about sub/supermartingales, we generalize to real Banach spaces which are order-closed, ordered monoids and ordered modules. This covers for instance n -> Real when Fintype n.

Estimated changes

Modified Mathlib/Probability/Martingale/Basic.lean

modified theorem MeasureTheory.Submartingale.condExp_sub_nonneg

modified theorem MeasureTheory.Submartingale.setIntegral_le

added theorem MeasureTheory.Submartingale.sum_smul_sub'

added theorem MeasureTheory.Submartingale.sum_smul_sub

modified theorem MeasureTheory.Submartingale.zero_le_of_predictable

modified theorem MeasureTheory.Supermartingale.le_zero_of_predictable

modified theorem MeasureTheory.Supermartingale.setIntegral_le

modified theorem MeasureTheory.martingale_nat

modified theorem MeasureTheory.martingale_of_condExp_sub_eq_zero_nat

modified theorem MeasureTheory.martingale_of_setIntegral_eq_succ

modified theorem MeasureTheory.submartingale_iff_condExp_sub_nonneg

modified theorem MeasureTheory.submartingale_nat

modified theorem MeasureTheory.submartingale_of_condExp_sub_nonneg

modified theorem MeasureTheory.submartingale_of_condExp_sub_nonneg_nat

modified theorem MeasureTheory.supermartingale_nat

modified theorem MeasureTheory.supermartingale_of_condExp_sub_nonneg_nat

Modified Mathlib/Probability/Process/Stopping.lean

modified theorem MeasureTheory.stoppedValue_piecewise_const'

modified theorem MeasureTheory.stoppedValue_piecewise_const