Documentation

Mathlib.Probability.Martingale.Basic

Martingales #

A family of functions f : ι → Ω → E is a martingale with respect to a filtration if every f i is integrable, f is adapted with respect to and for all i ≤ j, μ[f j | ℱ i] =ᵐ[μ] f i. On the other hand, f : ι → Ω → E is said to be a supermartingale with respect to the filtration if f i is integrable, f is adapted with resepct to and for all i ≤ j, μ[f j | ℱ i] ≤ᵐ[μ] f i. Finally, f : ι → Ω → E is said to be a submartingale with respect to the filtration if f i is integrable, f is adapted with resepct to and for all i ≤ j, f i ≤ᵐ[μ] μ[f j | ℱ i].

The definitions of filtration and adapted can be found in Probability.Process.Stopping.

Definitions #

Results #

def MeasureTheory.Martingale {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] (f : ιΩE) (ℱ : MeasureTheory.Filtration ι m0) (μ : MeasureTheory.Measure Ω) :

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

Equations
Instances For
    def MeasureTheory.Supermartingale {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] [LE E] (f : ιΩE) (ℱ : MeasureTheory.Filtration ι m0) (μ : MeasureTheory.Measure Ω) :

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

    Equations
    Instances For
      def MeasureTheory.Submartingale {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] [LE E] (f : ιΩE) (ℱ : MeasureTheory.Filtration ι m0) (μ : MeasureTheory.Measure Ω) :

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

      Equations
      Instances For
        theorem MeasureTheory.martingale_const {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] (ℱ : MeasureTheory.Filtration ι m0) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (x : E) :
        MeasureTheory.Martingale (fun (x_1 : ι) (x_2 : Ω) => x) μ
        theorem MeasureTheory.Martingale.adapted {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : ιΩE} {ℱ : MeasureTheory.Filtration ι m0} (hf : MeasureTheory.Martingale f μ) :
        theorem MeasureTheory.Martingale.stronglyMeasurable {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : ιΩE} {ℱ : MeasureTheory.Filtration ι m0} (hf : MeasureTheory.Martingale f μ) (i : ι) :
        theorem MeasureTheory.Martingale.condexp_ae_eq {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : ιΩE} {ℱ : MeasureTheory.Filtration ι m0} (hf : MeasureTheory.Martingale f μ) {i : ι} {j : ι} (hij : i j) :
        MeasureTheory.condexp ( i) μ (f j) =ᵐ[μ] f i
        theorem MeasureTheory.Martingale.integrable {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : ιΩE} {ℱ : MeasureTheory.Filtration ι m0} (hf : MeasureTheory.Martingale f μ) (i : ι) :
        theorem MeasureTheory.Martingale.setIntegral_eq {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : ιΩE} {ℱ : MeasureTheory.Filtration ι m0} [MeasureTheory.SigmaFiniteFiltration μ ] (hf : MeasureTheory.Martingale f μ) {i : ι} {j : ι} (hij : i j) {s : Set Ω} (hs : MeasurableSet s) :
        ∫ (ω : Ω) in s, f i ωμ = ∫ (ω : Ω) in s, f j ωμ
        @[deprecated MeasureTheory.Martingale.setIntegral_eq]
        theorem MeasureTheory.Martingale.set_integral_eq {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : ιΩE} {ℱ : MeasureTheory.Filtration ι m0} [MeasureTheory.SigmaFiniteFiltration μ ] (hf : MeasureTheory.Martingale f μ) {i : ι} {j : ι} (hij : i j) {s : Set Ω} (hs : MeasurableSet s) :
        ∫ (ω : Ω) in s, f i ωμ = ∫ (ω : Ω) in s, f j ωμ

        Alias of MeasureTheory.Martingale.setIntegral_eq.

        theorem MeasureTheory.Martingale.add {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : ιΩE} {g : ιΩE} {ℱ : MeasureTheory.Filtration ι m0} (hf : MeasureTheory.Martingale f μ) (hg : MeasureTheory.Martingale g μ) :
        theorem MeasureTheory.Martingale.neg {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : ιΩE} {ℱ : MeasureTheory.Filtration ι m0} (hf : MeasureTheory.Martingale f μ) :
        theorem MeasureTheory.Martingale.sub {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : ιΩE} {g : ιΩE} {ℱ : MeasureTheory.Filtration ι m0} (hf : MeasureTheory.Martingale f μ) (hg : MeasureTheory.Martingale g μ) :
        theorem MeasureTheory.Martingale.smul {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : ιΩE} {ℱ : MeasureTheory.Filtration ι m0} (c : ) (hf : MeasureTheory.Martingale f μ) :
        theorem MeasureTheory.Martingale.supermartingale {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : ιΩE} {ℱ : MeasureTheory.Filtration ι m0} [Preorder E] (hf : MeasureTheory.Martingale f μ) :
        theorem MeasureTheory.Martingale.submartingale {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : ιΩE} {ℱ : MeasureTheory.Filtration ι m0} [Preorder E] (hf : MeasureTheory.Martingale f μ) :
        theorem MeasureTheory.martingale_condexp {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] (f : ΩE) (ℱ : MeasureTheory.Filtration ι m0) (μ : MeasureTheory.Measure Ω) [MeasureTheory.SigmaFiniteFiltration μ ] :
        MeasureTheory.Martingale (fun (i : ι) => MeasureTheory.condexp ( i) μ f) μ
        theorem MeasureTheory.Supermartingale.adapted {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : ιΩE} {ℱ : MeasureTheory.Filtration ι m0} [LE E] (hf : MeasureTheory.Supermartingale f μ) :
        theorem MeasureTheory.Supermartingale.stronglyMeasurable {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : ιΩE} {ℱ : MeasureTheory.Filtration ι m0} [LE E] (hf : MeasureTheory.Supermartingale f μ) (i : ι) :
        theorem MeasureTheory.Supermartingale.integrable {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : ιΩE} {ℱ : MeasureTheory.Filtration ι m0} [LE E] (hf : MeasureTheory.Supermartingale f μ) (i : ι) :
        theorem MeasureTheory.Supermartingale.condexp_ae_le {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : ιΩE} {ℱ : MeasureTheory.Filtration ι m0} [LE E] (hf : MeasureTheory.Supermartingale f μ) {i : ι} {j : ι} (hij : i j) :
        MeasureTheory.condexp ( i) μ (f j) ≤ᵐ[μ] f i
        theorem MeasureTheory.Supermartingale.setIntegral_le {Ω : Type u_1} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ι m0} [MeasureTheory.SigmaFiniteFiltration μ ] {f : ιΩ} (hf : MeasureTheory.Supermartingale f μ) {i : ι} {j : ι} (hij : i j) {s : Set Ω} (hs : MeasurableSet s) :
        ∫ (ω : Ω) in s, f j ωμ ∫ (ω : Ω) in s, f i ωμ
        @[deprecated MeasureTheory.Supermartingale.setIntegral_le]
        theorem MeasureTheory.Supermartingale.set_integral_le {Ω : Type u_1} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ι m0} [MeasureTheory.SigmaFiniteFiltration μ ] {f : ιΩ} (hf : MeasureTheory.Supermartingale f μ) {i : ι} {j : ι} (hij : i j) {s : Set Ω} (hs : MeasurableSet s) :
        ∫ (ω : Ω) in s, f j ωμ ∫ (ω : Ω) in s, f i ωμ

        Alias of MeasureTheory.Supermartingale.setIntegral_le.

        theorem MeasureTheory.Supermartingale.add {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : ιΩE} {g : ιΩE} {ℱ : MeasureTheory.Filtration ι m0} [Preorder E] [AddLeftMono E] (hf : MeasureTheory.Supermartingale f μ) (hg : MeasureTheory.Supermartingale g μ) :
        theorem MeasureTheory.Supermartingale.add_martingale {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : ιΩE} {g : ιΩE} {ℱ : MeasureTheory.Filtration ι m0} [Preorder E] [AddLeftMono E] (hf : MeasureTheory.Supermartingale f μ) (hg : MeasureTheory.Martingale g μ) :
        theorem MeasureTheory.Supermartingale.neg {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : ιΩE} {ℱ : MeasureTheory.Filtration ι m0} [Preorder E] [AddLeftMono E] (hf : MeasureTheory.Supermartingale f μ) :
        theorem MeasureTheory.Submartingale.adapted {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : ιΩE} {ℱ : MeasureTheory.Filtration ι m0} [LE E] (hf : MeasureTheory.Submartingale f μ) :
        theorem MeasureTheory.Submartingale.stronglyMeasurable {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : ιΩE} {ℱ : MeasureTheory.Filtration ι m0} [LE E] (hf : MeasureTheory.Submartingale f μ) (i : ι) :
        theorem MeasureTheory.Submartingale.integrable {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : ιΩE} {ℱ : MeasureTheory.Filtration ι m0} [LE E] (hf : MeasureTheory.Submartingale f μ) (i : ι) :
        theorem MeasureTheory.Submartingale.ae_le_condexp {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : ιΩE} {ℱ : MeasureTheory.Filtration ι m0} [LE E] (hf : MeasureTheory.Submartingale f μ) {i : ι} {j : ι} (hij : i j) :
        f i ≤ᵐ[μ] MeasureTheory.condexp ( i) μ (f j)
        theorem MeasureTheory.Submartingale.add {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : ιΩE} {g : ιΩE} {ℱ : MeasureTheory.Filtration ι m0} [Preorder E] [AddLeftMono E] (hf : MeasureTheory.Submartingale f μ) (hg : MeasureTheory.Submartingale g μ) :
        theorem MeasureTheory.Submartingale.add_martingale {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : ιΩE} {g : ιΩE} {ℱ : MeasureTheory.Filtration ι m0} [Preorder E] [AddLeftMono E] (hf : MeasureTheory.Submartingale f μ) (hg : MeasureTheory.Martingale g μ) :
        theorem MeasureTheory.Submartingale.neg {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : ιΩE} {ℱ : MeasureTheory.Filtration ι m0} [Preorder E] [AddLeftMono E] (hf : MeasureTheory.Submartingale f μ) :
        theorem MeasureTheory.Submartingale.setIntegral_le {Ω : Type u_1} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ι m0} [MeasureTheory.SigmaFiniteFiltration μ ] {f : ιΩ} (hf : MeasureTheory.Submartingale f μ) {i : ι} {j : ι} (hij : i j) {s : Set Ω} (hs : MeasurableSet s) :
        ∫ (ω : Ω) in s, f i ωμ ∫ (ω : Ω) in s, f j ωμ

        The converse of this lemma is MeasureTheory.submartingale_of_setIntegral_le.

        @[deprecated MeasureTheory.Submartingale.setIntegral_le]
        theorem MeasureTheory.Submartingale.set_integral_le {Ω : Type u_1} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ι m0} [MeasureTheory.SigmaFiniteFiltration μ ] {f : ιΩ} (hf : MeasureTheory.Submartingale f μ) {i : ι} {j : ι} (hij : i j) {s : Set Ω} (hs : MeasurableSet s) :
        ∫ (ω : Ω) in s, f i ωμ ∫ (ω : Ω) in s, f j ωμ

        Alias of MeasureTheory.Submartingale.setIntegral_le.


        The converse of this lemma is MeasureTheory.submartingale_of_setIntegral_le.

        theorem MeasureTheory.Submartingale.sub_supermartingale {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : ιΩE} {g : ιΩE} {ℱ : MeasureTheory.Filtration ι m0} [Preorder E] [AddLeftMono E] (hf : MeasureTheory.Submartingale f μ) (hg : MeasureTheory.Supermartingale g μ) :
        theorem MeasureTheory.Submartingale.sub_martingale {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : ιΩE} {g : ιΩE} {ℱ : MeasureTheory.Filtration ι m0} [Preorder E] [AddLeftMono E] (hf : MeasureTheory.Submartingale f μ) (hg : MeasureTheory.Martingale g μ) :
        theorem MeasureTheory.Submartingale.sup {Ω : Type u_1} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ι m0} {f : ιΩ} {g : ιΩ} (hf : MeasureTheory.Submartingale f μ) (hg : MeasureTheory.Submartingale g μ) :
        theorem MeasureTheory.Submartingale.pos {Ω : Type u_1} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ι m0} {f : ιΩ} (hf : MeasureTheory.Submartingale f μ) :
        theorem MeasureTheory.submartingale_of_setIntegral_le {Ω : Type u_1} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ι m0} [MeasureTheory.IsFiniteMeasure μ] {f : ιΩ} (hadp : MeasureTheory.Adapted f) (hint : ∀ (i : ι), MeasureTheory.Integrable (f i) μ) (hf : ∀ (i j : ι), i j∀ (s : Set Ω), MeasurableSet s∫ (ω : Ω) in s, f i ωμ ∫ (ω : Ω) in s, f j ωμ) :
        @[deprecated MeasureTheory.submartingale_of_setIntegral_le]
        theorem MeasureTheory.submartingale_of_set_integral_le {Ω : Type u_1} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ι m0} [MeasureTheory.IsFiniteMeasure μ] {f : ιΩ} (hadp : MeasureTheory.Adapted f) (hint : ∀ (i : ι), MeasureTheory.Integrable (f i) μ) (hf : ∀ (i j : ι), i j∀ (s : Set Ω), MeasurableSet s∫ (ω : Ω) in s, f i ωμ ∫ (ω : Ω) in s, f j ωμ) :

        Alias of MeasureTheory.submartingale_of_setIntegral_le.

        theorem MeasureTheory.submartingale_of_condexp_sub_nonneg {Ω : Type u_1} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ι m0} [MeasureTheory.IsFiniteMeasure μ] {f : ιΩ} (hadp : MeasureTheory.Adapted f) (hint : ∀ (i : ι), MeasureTheory.Integrable (f i) μ) (hf : ∀ (i j : ι), i j0 ≤ᵐ[μ] MeasureTheory.condexp ( i) μ (f j - f i)) :
        theorem MeasureTheory.Submartingale.condexp_sub_nonneg {Ω : Type u_1} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ι m0} {f : ιΩ} (hf : MeasureTheory.Submartingale f μ) {i : ι} {j : ι} (hij : i j) :
        0 ≤ᵐ[μ] MeasureTheory.condexp ( i) μ (f j - f i)
        theorem MeasureTheory.submartingale_iff_condexp_sub_nonneg {Ω : Type u_1} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ι m0} [MeasureTheory.IsFiniteMeasure μ] {f : ιΩ} :
        MeasureTheory.Submartingale f μ MeasureTheory.Adapted f (∀ (i : ι), MeasureTheory.Integrable (f i) μ) ∀ (i j : ι), i j0 ≤ᵐ[μ] MeasureTheory.condexp ( i) μ (f j - f i)
        theorem MeasureTheory.Supermartingale.sub_submartingale {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : ιΩE} {g : ιΩE} {ℱ : MeasureTheory.Filtration ι m0} [Preorder E] [AddLeftMono E] (hf : MeasureTheory.Supermartingale f μ) (hg : MeasureTheory.Submartingale g μ) :
        theorem MeasureTheory.Supermartingale.sub_martingale {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : ιΩE} {g : ιΩE} {ℱ : MeasureTheory.Filtration ι m0} [Preorder E] [AddLeftMono E] (hf : MeasureTheory.Supermartingale f μ) (hg : MeasureTheory.Martingale g μ) :
        theorem MeasureTheory.Supermartingale.smul_nonneg {Ω : Type u_1} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ι m0} {F : Type u_4} [NormedLatticeAddCommGroup F] [NormedSpace F] [CompleteSpace F] [OrderedSMul F] {f : ιΩF} {c : } (hc : 0 c) (hf : MeasureTheory.Supermartingale f μ) :
        theorem MeasureTheory.Supermartingale.smul_nonpos {Ω : Type u_1} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ι m0} {F : Type u_4} [NormedLatticeAddCommGroup F] [NormedSpace F] [CompleteSpace F] [OrderedSMul F] {f : ιΩF} {c : } (hc : c 0) (hf : MeasureTheory.Supermartingale f μ) :
        theorem MeasureTheory.Submartingale.smul_nonneg {Ω : Type u_1} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ι m0} {F : Type u_4} [NormedLatticeAddCommGroup F] [NormedSpace F] [CompleteSpace F] [OrderedSMul F] {f : ιΩF} {c : } (hc : 0 c) (hf : MeasureTheory.Submartingale f μ) :
        theorem MeasureTheory.Submartingale.smul_nonpos {Ω : Type u_1} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ι m0} {F : Type u_4} [NormedLatticeAddCommGroup F] [NormedSpace F] [CompleteSpace F] [OrderedSMul F] {f : ιΩF} {c : } (hc : c 0) (hf : MeasureTheory.Submartingale f μ) :
        theorem MeasureTheory.submartingale_of_setIntegral_le_succ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration m0} [MeasureTheory.IsFiniteMeasure μ] {f : Ω} (hadp : MeasureTheory.Adapted 𝒢 f) (hint : ∀ (i : ), MeasureTheory.Integrable (f i) μ) (hf : ∀ (i : ) (s : Set Ω), MeasurableSet s∫ (ω : Ω) in s, f i ωμ ∫ (ω : Ω) in s, f (i + 1) ωμ) :
        @[deprecated MeasureTheory.submartingale_of_setIntegral_le_succ]
        theorem MeasureTheory.submartingale_of_set_integral_le_succ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration m0} [MeasureTheory.IsFiniteMeasure μ] {f : Ω} (hadp : MeasureTheory.Adapted 𝒢 f) (hint : ∀ (i : ), MeasureTheory.Integrable (f i) μ) (hf : ∀ (i : ) (s : Set Ω), MeasurableSet s∫ (ω : Ω) in s, f i ωμ ∫ (ω : Ω) in s, f (i + 1) ωμ) :

        Alias of MeasureTheory.submartingale_of_setIntegral_le_succ.

        theorem MeasureTheory.supermartingale_of_setIntegral_succ_le {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration m0} [MeasureTheory.IsFiniteMeasure μ] {f : Ω} (hadp : MeasureTheory.Adapted 𝒢 f) (hint : ∀ (i : ), MeasureTheory.Integrable (f i) μ) (hf : ∀ (i : ) (s : Set Ω), MeasurableSet s∫ (ω : Ω) in s, f (i + 1) ωμ ∫ (ω : Ω) in s, f i ωμ) :
        @[deprecated MeasureTheory.supermartingale_of_setIntegral_succ_le]
        theorem MeasureTheory.supermartingale_of_set_integral_succ_le {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration m0} [MeasureTheory.IsFiniteMeasure μ] {f : Ω} (hadp : MeasureTheory.Adapted 𝒢 f) (hint : ∀ (i : ), MeasureTheory.Integrable (f i) μ) (hf : ∀ (i : ) (s : Set Ω), MeasurableSet s∫ (ω : Ω) in s, f (i + 1) ωμ ∫ (ω : Ω) in s, f i ωμ) :

        Alias of MeasureTheory.supermartingale_of_setIntegral_succ_le.

        theorem MeasureTheory.martingale_of_setIntegral_eq_succ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration m0} [MeasureTheory.IsFiniteMeasure μ] {f : Ω} (hadp : MeasureTheory.Adapted 𝒢 f) (hint : ∀ (i : ), MeasureTheory.Integrable (f i) μ) (hf : ∀ (i : ) (s : Set Ω), MeasurableSet s∫ (ω : Ω) in s, f i ωμ = ∫ (ω : Ω) in s, f (i + 1) ωμ) :
        @[deprecated MeasureTheory.martingale_of_setIntegral_eq_succ]
        theorem MeasureTheory.martingale_of_set_integral_eq_succ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration m0} [MeasureTheory.IsFiniteMeasure μ] {f : Ω} (hadp : MeasureTheory.Adapted 𝒢 f) (hint : ∀ (i : ), MeasureTheory.Integrable (f i) μ) (hf : ∀ (i : ) (s : Set Ω), MeasurableSet s∫ (ω : Ω) in s, f i ωμ = ∫ (ω : Ω) in s, f (i + 1) ωμ) :

        Alias of MeasureTheory.martingale_of_setIntegral_eq_succ.

        theorem MeasureTheory.submartingale_nat {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration m0} [MeasureTheory.IsFiniteMeasure μ] {f : Ω} (hadp : MeasureTheory.Adapted 𝒢 f) (hint : ∀ (i : ), MeasureTheory.Integrable (f i) μ) (hf : ∀ (i : ), f i ≤ᵐ[μ] MeasureTheory.condexp (𝒢 i) μ (f (i + 1))) :
        theorem MeasureTheory.supermartingale_nat {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration m0} [MeasureTheory.IsFiniteMeasure μ] {f : Ω} (hadp : MeasureTheory.Adapted 𝒢 f) (hint : ∀ (i : ), MeasureTheory.Integrable (f i) μ) (hf : ∀ (i : ), MeasureTheory.condexp (𝒢 i) μ (f (i + 1)) ≤ᵐ[μ] f i) :
        theorem MeasureTheory.martingale_nat {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration m0} [MeasureTheory.IsFiniteMeasure μ] {f : Ω} (hadp : MeasureTheory.Adapted 𝒢 f) (hint : ∀ (i : ), MeasureTheory.Integrable (f i) μ) (hf : ∀ (i : ), f i =ᵐ[μ] MeasureTheory.condexp (𝒢 i) μ (f (i + 1))) :
        theorem MeasureTheory.submartingale_of_condexp_sub_nonneg_nat {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration m0} [MeasureTheory.IsFiniteMeasure μ] {f : Ω} (hadp : MeasureTheory.Adapted 𝒢 f) (hint : ∀ (i : ), MeasureTheory.Integrable (f i) μ) (hf : ∀ (i : ), 0 ≤ᵐ[μ] MeasureTheory.condexp (𝒢 i) μ (f (i + 1) - f i)) :
        theorem MeasureTheory.supermartingale_of_condexp_sub_nonneg_nat {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration m0} [MeasureTheory.IsFiniteMeasure μ] {f : Ω} (hadp : MeasureTheory.Adapted 𝒢 f) (hint : ∀ (i : ), MeasureTheory.Integrable (f i) μ) (hf : ∀ (i : ), 0 ≤ᵐ[μ] MeasureTheory.condexp (𝒢 i) μ (f i - f (i + 1))) :
        theorem MeasureTheory.martingale_of_condexp_sub_eq_zero_nat {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration m0} [MeasureTheory.IsFiniteMeasure μ] {f : Ω} (hadp : MeasureTheory.Adapted 𝒢 f) (hint : ∀ (i : ), MeasureTheory.Integrable (f i) μ) (hf : ∀ (i : ), MeasureTheory.condexp (𝒢 i) μ (f (i + 1) - f i) =ᵐ[μ] 0) :
        theorem MeasureTheory.Submartingale.zero_le_of_predictable {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {𝒢 : MeasureTheory.Filtration m0} [Preorder E] [MeasureTheory.SigmaFiniteFiltration μ 𝒢] {f : ΩE} (hfmgle : MeasureTheory.Submartingale f 𝒢 μ) (hfadp : MeasureTheory.Adapted 𝒢 fun (n : ) => f (n + 1)) (n : ) :
        f 0 ≤ᵐ[μ] f n

        A predictable submartingale is a.e. greater equal than its initial state.

        theorem MeasureTheory.Supermartingale.le_zero_of_predictable {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {𝒢 : MeasureTheory.Filtration m0} [Preorder E] [MeasureTheory.SigmaFiniteFiltration μ 𝒢] {f : ΩE} (hfmgle : MeasureTheory.Supermartingale f 𝒢 μ) (hfadp : MeasureTheory.Adapted 𝒢 fun (n : ) => f (n + 1)) (n : ) :
        f n ≤ᵐ[μ] f 0

        A predictable supermartingale is a.e. less equal than its initial state.

        theorem MeasureTheory.Martingale.eq_zero_of_predictable {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {𝒢 : MeasureTheory.Filtration m0} [MeasureTheory.SigmaFiniteFiltration μ 𝒢] {f : ΩE} (hfmgle : MeasureTheory.Martingale f 𝒢 μ) (hfadp : MeasureTheory.Adapted 𝒢 fun (n : ) => f (n + 1)) (n : ) :
        f n =ᵐ[μ] f 0

        A predictable martingale is a.e. equal to its initial state.

        theorem MeasureTheory.Submartingale.integrable_stoppedValue {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {𝒢 : MeasureTheory.Filtration m0} [LE E] {f : ΩE} (hf : MeasureTheory.Submartingale f 𝒢 μ) {τ : Ω} (hτ : MeasureTheory.IsStoppingTime 𝒢 τ) {N : } (hbdd : ∀ (ω : Ω), τ ω N) :
        theorem MeasureTheory.Submartingale.sum_mul_sub {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration m0} [MeasureTheory.IsFiniteMeasure μ] {R : } {ξ : Ω} {f : Ω} (hf : MeasureTheory.Submartingale f 𝒢 μ) (hξ : MeasureTheory.Adapted 𝒢 ξ) (hbdd : ∀ (n : ) (ω : Ω), ξ n ω R) (hnonneg : ∀ (n : ) (ω : Ω), 0 ξ n ω) :
        MeasureTheory.Submartingale (fun (n : ) => kFinset.range n, ξ k * (f (k + 1) - f k)) 𝒢 μ
        theorem MeasureTheory.Submartingale.sum_mul_sub' {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration m0} [MeasureTheory.IsFiniteMeasure μ] {R : } {ξ : Ω} {f : Ω} (hf : MeasureTheory.Submartingale f 𝒢 μ) (hξ : MeasureTheory.Adapted 𝒢 fun (n : ) => ξ (n + 1)) (hbdd : ∀ (n : ) (ω : Ω), ξ n ω R) (hnonneg : ∀ (n : ) (ω : Ω), 0 ξ n ω) :
        MeasureTheory.Submartingale (fun (n : ) => kFinset.range n, ξ (k + 1) * (f (k + 1) - f k)) 𝒢 μ

        Given a discrete submartingale f and a predictable process ξ (i.e. ξ (n + 1) is adapted) the process defined by fun n => ∑ k ∈ Finset.range n, ξ (k + 1) * (f (k + 1) - f k) is also a submartingale.