Theorems · Definition · probability

MeasureTheory.Martingale

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

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

Defined in

Mathlib.Probability.Martingale.Basic

Cited by

46 results in Mathlib

Foundations

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

Assumes

PreorderNormedAddCommGroupNormedSpace