Theorems · Definition · probability

MeasureTheory.Submartingale

{Ω : Type u_1} →
  {E : Type u_2} →
    {ι : Type u_3} →
      [inst : Preorder ι] →
        {m0 : MeasurableSpace Ω} →
          [inst_1 : NormedAddCommGroup E] →
            [NormedSpace ℝ E] → [LE E] → (ι → Ω → E) → MeasureTheory.Filtration ι m0 → MeasureTheory.Measure Ω → Prop

A family of integrable functions f : ι → Ω → E is a submartingale with respect to a filtration ℱ if f is strongly adapted with respect to ℱ and for all i ≤ j, f i ≤ᵐ[μ] μ[f j | ℱ.le i].

Defined in

Mathlib.Probability.Martingale.Basic

Cited by

63 results in Mathlib

Foundations

Depth 294 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PreorderNormedAddCommGroupNormedSpaceLE