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 respect 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 respect 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 #

MeasureTheory.Martingale f ℱ μ: f is a martingale with respect to filtration ℱ and measure μ.
MeasureTheory.Supermartingale f ℱ μ: f is a supermartingale with respect to filtration ℱ and measure μ.
MeasureTheory.Submartingale f ℱ μ: f is a submartingale with respect to filtration ℱ and measure μ.

Results #

MeasureTheory.martingale_condExp f ℱ μ: the sequence fun i => μ[f | ℱ i, ℱ.le i]) is a martingale with respect to ℱ and μ.

def MeasureTheory.Martingale {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (f : ι → Ω → E) (ℱ : Filtration ι m0) (μ : 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

MeasureTheory.Martingale f ℱ μ = (MeasureTheory.Adapted ℱ f ∧ ∀ (i j : ι), i ≤ j → μ[f j|↑ℱ i] =ᵐ[μ] f i)

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) (ℱ : Filtration ι m0) (μ : 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

MeasureTheory.Supermartingale f ℱ μ = (MeasureTheory.Adapted ℱ f ∧ (∀ (i j : ι), i ≤ j → μ[f j|↑ℱ i] ≤ᵐ[μ] f i) ∧ ∀ (i : ι), MeasureTheory.Integrable (f i) μ)

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) (ℱ : Filtration ι m0) (μ : 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

MeasureTheory.Submartingale f ℱ μ = (MeasureTheory.Adapted ℱ f ∧ (∀ (i j : ι), i ≤ j → f i ≤ᵐ[μ] μ[f j|↑ℱ i]) ∧ ∀ (i : ι), MeasureTheory.Integrable (f i) μ)

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] (ℱ : Filtration ι m0) (μ : Measure Ω) [IsFiniteMeasure μ] (x : E) :

Martingale (fun (x_1 : ι) (x_2 : Ω) => x) ℱ μ

theorem MeasureTheory.martingale_const_fun {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [OrderBot ι] (ℱ : Filtration ι m0) (μ : Measure Ω) [SigmaFiniteFiltration μ ℱ] {f : Ω → E} (hf : StronglyMeasurable f) (hfint : Integrable f μ) :

Martingale (fun (x : ι) => f) ℱ μ

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

Martingale 0 ℱ μ

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

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

StronglyMeasurable (f i)

theorem MeasureTheory.Martingale.condExp_ae_eq {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ι → Ω → E} {ℱ : Filtration ι m0} (hf : Martingale f ℱ μ) {i j : ι} (hij : i ≤ j) :

μ[f j|↑ℱ i] =ᶠ[ae μ] f i

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

Integrable (f i) μ

theorem MeasureTheory.Martingale.setIntegral_eq {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ι → Ω → E} {ℱ : Filtration ι m0} [SigmaFiniteFiltration μ ℱ] (hf : Martingale f ℱ μ) {i j : ι} (hij : i ≤ j) {s : Set Ω} (hs : MeasurableSet s) :

∫ (ω : Ω) in s, f i ω ∂μ = ∫ (ω : Ω) in s, f j ω ∂μ

theorem MeasureTheory.Martingale.add {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f g : ι → Ω → E} {ℱ : Filtration ι m0} (hf : Martingale f ℱ μ) (hg : Martingale g ℱ μ) :

Martingale (f + g) ℱ μ

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

Martingale (-f) ℱ μ

theorem MeasureTheory.Martingale.sub {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f g : ι → Ω → E} {ℱ : Filtration ι m0} (hf : Martingale f ℱ μ) (hg : Martingale g ℱ μ) :

Martingale (f - g) ℱ μ

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

Martingale (c • f) ℱ μ

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

Supermartingale f ℱ μ

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

Submartingale f ℱ μ

theorem MeasureTheory.martingale_iff {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ι → Ω → E} {ℱ : Filtration ι m0} [PartialOrder E] :

Martingale f ℱ μ ↔ Supermartingale f ℱ μ ∧ Submartingale 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) (ℱ : Filtration ι m0) (μ : Measure Ω) [SigmaFiniteFiltration μ ℱ] :

Martingale (fun (i : ι) => μ[f|↑ℱ i]) ℱ μ

theorem MeasureTheory.Supermartingale.adapted {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ι → Ω → E} {ℱ : Filtration ι m0} [LE E] (hf : Supermartingale f ℱ μ) :

theorem MeasureTheory.Supermartingale.stronglyMeasurable {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ι → Ω → E} {ℱ : Filtration ι m0} [LE E] (hf : Supermartingale f ℱ μ) (i : ι) :

StronglyMeasurable (f i)

theorem MeasureTheory.Supermartingale.integrable {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ι → Ω → E} {ℱ : Filtration ι m0} [LE E] (hf : Supermartingale f ℱ μ) (i : ι) :

Integrable (f i) μ

theorem MeasureTheory.Supermartingale.condExp_ae_le {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ι → Ω → E} {ℱ : Filtration ι m0} [LE E] (hf : Supermartingale f ℱ μ) {i j : ι} (hij : i ≤ j) :

μ[f j|↑ℱ i] ≤ᶠ[ae μ] f i

theorem MeasureTheory.Supermartingale.setIntegral_le {Ω : Type u_1} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : Measure Ω} {ℱ : Filtration ι m0} [SigmaFiniteFiltration μ ℱ] {f : ι → Ω → ℝ} (hf : Supermartingale f ℱ μ) {i j : ι} (hij : i ≤ j) {s : Set Ω} (hs : MeasurableSet s) :

∫ (ω : Ω) in s, f j ω ∂μ ≤ ∫ (ω : Ω) in s, f i ω ∂μ

theorem MeasureTheory.Supermartingale.add {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f g : ι → Ω → E} {ℱ : Filtration ι m0} [Preorder E] [AddLeftMono E] (hf : Supermartingale f ℱ μ) (hg : Supermartingale g ℱ μ) :

Supermartingale (f + g) ℱ μ

theorem MeasureTheory.Supermartingale.add_martingale {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f g : ι → Ω → E} {ℱ : Filtration ι m0} [Preorder E] [AddLeftMono E] (hf : Supermartingale f ℱ μ) (hg : Martingale g ℱ μ) :

Supermartingale (f + g) ℱ μ

theorem MeasureTheory.Supermartingale.neg {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ι → Ω → E} {ℱ : Filtration ι m0} [Preorder E] [AddLeftMono E] (hf : Supermartingale f ℱ μ) :

Submartingale (-f) ℱ μ

theorem MeasureTheory.Submartingale.adapted {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ι → Ω → E} {ℱ : Filtration ι m0} [LE E] (hf : Submartingale f ℱ μ) :

theorem MeasureTheory.Submartingale.stronglyMeasurable {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ι → Ω → E} {ℱ : Filtration ι m0} [LE E] (hf : Submartingale f ℱ μ) (i : ι) :

StronglyMeasurable (f i)

theorem MeasureTheory.Submartingale.integrable {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ι → Ω → E} {ℱ : Filtration ι m0} [LE E] (hf : Submartingale f ℱ μ) (i : ι) :

Integrable (f i) μ

theorem MeasureTheory.Submartingale.ae_le_condExp {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ι → Ω → E} {ℱ : Filtration ι m0} [LE E] (hf : Submartingale f ℱ μ) {i j : ι} (hij : i ≤ j) :

f i ≤ᶠ[ae μ] μ[f j|↑ℱ i]

theorem MeasureTheory.Submartingale.add {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f g : ι → Ω → E} {ℱ : Filtration ι m0} [Preorder E] [AddLeftMono E] (hf : Submartingale f ℱ μ) (hg : Submartingale g ℱ μ) :

Submartingale (f + g) ℱ μ

theorem MeasureTheory.Submartingale.add_martingale {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f g : ι → Ω → E} {ℱ : Filtration ι m0} [Preorder E] [AddLeftMono E] (hf : Submartingale f ℱ μ) (hg : Martingale g ℱ μ) :

Submartingale (f + g) ℱ μ

theorem MeasureTheory.Submartingale.neg {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ι → Ω → E} {ℱ : Filtration ι m0} [Preorder E] [AddLeftMono E] (hf : Submartingale f ℱ μ) :

Supermartingale (-f) ℱ μ

theorem MeasureTheory.Submartingale.setIntegral_le {Ω : Type u_1} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : Measure Ω} {ℱ : Filtration ι m0} [SigmaFiniteFiltration μ ℱ] {f : ι → Ω → ℝ} (hf : 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.

theorem MeasureTheory.Submartingale.sub_supermartingale {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f g : ι → Ω → E} {ℱ : Filtration ι m0} [Preorder E] [AddLeftMono E] (hf : Submartingale f ℱ μ) (hg : Supermartingale g ℱ μ) :

Submartingale (f - g) ℱ μ

theorem MeasureTheory.Submartingale.sub_martingale {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f g : ι → Ω → E} {ℱ : Filtration ι m0} [Preorder E] [AddLeftMono E] (hf : Submartingale f ℱ μ) (hg : Martingale g ℱ μ) :

Submartingale (f - g) ℱ μ

theorem MeasureTheory.Submartingale.sup {Ω : Type u_1} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : Measure Ω} {ℱ : Filtration ι m0} {f g : ι → Ω → ℝ} (hf : Submartingale f ℱ μ) (hg : Submartingale g ℱ μ) :

Submartingale (f ⊔ g) ℱ μ

theorem MeasureTheory.Submartingale.pos {Ω : Type u_1} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : Measure Ω} {ℱ : Filtration ι m0} {f : ι → Ω → ℝ} (hf : Submartingale f ℱ μ) :

Submartingale f⁺ ℱ μ

theorem MeasureTheory.submartingale_of_setIntegral_le {Ω : Type u_1} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : Measure Ω} {ℱ : Filtration ι m0} [SigmaFiniteFiltration μ ℱ] {f : ι → Ω → ℝ} (hadp : Adapted ℱ f) (hint : ∀ (i : ι), Integrable (f i) μ) (hf : ∀ (i j : ι), i ≤ j → ∀ (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f j ω ∂μ) :

Submartingale f ℱ μ

theorem MeasureTheory.submartingale_of_condExp_sub_nonneg {Ω : Type u_1} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : Measure Ω} {ℱ : Filtration ι m0} [SigmaFiniteFiltration μ ℱ] {f : ι → Ω → ℝ} (hadp : Adapted ℱ f) (hint : ∀ (i : ι), Integrable (f i) μ) (hf : ∀ (i j : ι), i ≤ j → 0 ≤ᶠ[ae μ] μ[f j - f i|↑ℱ i]) :

Submartingale f ℱ μ

theorem MeasureTheory.Submartingale.condExp_sub_nonneg {Ω : Type u_1} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : Measure Ω} {ℱ : Filtration ι m0} {f : ι → Ω → ℝ} (hf : Submartingale f ℱ μ) {i j : ι} (hij : i ≤ j) :

0 ≤ᶠ[ae μ] μ[f j - f i|↑ℱ i]

theorem MeasureTheory.submartingale_iff_condExp_sub_nonneg {Ω : Type u_1} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : Measure Ω} {ℱ : Filtration ι m0} [SigmaFiniteFiltration μ ℱ] {f : ι → Ω → ℝ} :

Submartingale f ℱ μ ↔ Adapted ℱ f ∧ (∀ (i : ι), Integrable (f i) μ) ∧ ∀ (i j : ι), i ≤ j → 0 ≤ᶠ[ae μ] μ[f j - f i|↑ℱ i]

theorem MeasureTheory.Supermartingale.sub_submartingale {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f g : ι → Ω → E} {ℱ : Filtration ι m0} [Preorder E] [AddLeftMono E] (hf : Supermartingale f ℱ μ) (hg : Submartingale g ℱ μ) :

Supermartingale (f - g) ℱ μ

theorem MeasureTheory.Supermartingale.sub_martingale {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f g : ι → Ω → E} {ℱ : Filtration ι m0} [Preorder E] [AddLeftMono E] (hf : Supermartingale f ℱ μ) (hg : Martingale g ℱ μ) :

Supermartingale (f - g) ℱ μ

theorem MeasureTheory.Supermartingale.smul_nonneg {Ω : Type u_1} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : Measure Ω} {ℱ : Filtration ι m0} {F : Type u_4} [NormedAddCommGroup F] [Lattice F] [NormedSpace ℝ F] [CompleteSpace F] [IsOrderedModule ℝ F] {f : ι → Ω → F} {c : ℝ} (hc : 0 ≤ c) (hf : Supermartingale f ℱ μ) :

Supermartingale (c • f) ℱ μ

theorem MeasureTheory.Supermartingale.smul_nonpos {Ω : Type u_1} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : Measure Ω} {ℱ : Filtration ι m0} {F : Type u_4} [NormedAddCommGroup F] [Lattice F] [NormedSpace ℝ F] [CompleteSpace F] [IsOrderedModule ℝ F] [IsOrderedAddMonoid F] {f : ι → Ω → F} {c : ℝ} (hc : c ≤ 0) (hf : Supermartingale f ℱ μ) :

Submartingale (c • f) ℱ μ

theorem MeasureTheory.Submartingale.smul_nonneg {Ω : Type u_1} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : Measure Ω} {ℱ : Filtration ι m0} {F : Type u_4} [NormedAddCommGroup F] [Lattice F] [IsOrderedAddMonoid F] [NormedSpace ℝ F] [CompleteSpace F] [IsOrderedModule ℝ F] {f : ι → Ω → F} {c : ℝ} (hc : 0 ≤ c) (hf : Submartingale f ℱ μ) :

Submartingale (c • f) ℱ μ

theorem MeasureTheory.Submartingale.smul_nonpos {Ω : Type u_1} {ι : Type u_3} [Preorder ι] {m0 : MeasurableSpace Ω} {μ : Measure Ω} {ℱ : Filtration ι m0} {F : Type u_4} [NormedAddCommGroup F] [Lattice F] [IsOrderedAddMonoid F] [NormedSpace ℝ F] [CompleteSpace F] [IsOrderedModule ℝ F] {f : ι → Ω → F} {c : ℝ} (hc : c ≤ 0) (hf : Submartingale f ℱ μ) :

Supermartingale (c • f) ℱ μ

theorem MeasureTheory.submartingale_of_setIntegral_le_succ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : Measure Ω} {𝒢 : Filtration ℕ m0} [IsFiniteMeasure μ] {f : ℕ → Ω → ℝ} (hadp : Adapted 𝒢 f) (hint : ∀ (i : ℕ), Integrable (f i) μ) (hf : ∀ (i : ℕ) (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f (i + 1) ω ∂μ) :

Submartingale f 𝒢 μ

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

Supermartingale f 𝒢 μ

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

Martingale f 𝒢 μ

theorem MeasureTheory.submartingale_nat {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : Measure Ω} {𝒢 : Filtration ℕ m0} [IsFiniteMeasure μ] {f : ℕ → Ω → ℝ} (hadp : Adapted 𝒢 f) (hint : ∀ (i : ℕ), Integrable (f i) μ) (hf : ∀ (i : ℕ), f i ≤ᶠ[ae μ] μ[f (i + 1)|↑𝒢 i]) :

Submartingale f 𝒢 μ

theorem MeasureTheory.supermartingale_nat {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : Measure Ω} {𝒢 : Filtration ℕ m0} [IsFiniteMeasure μ] {f : ℕ → Ω → ℝ} (hadp : Adapted 𝒢 f) (hint : ∀ (i : ℕ), Integrable (f i) μ) (hf : ∀ (i : ℕ), μ[f (i + 1)|↑𝒢 i] ≤ᶠ[ae μ] f i) :

Supermartingale f 𝒢 μ

theorem MeasureTheory.martingale_nat {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : Measure Ω} {𝒢 : Filtration ℕ m0} [IsFiniteMeasure μ] {f : ℕ → Ω → ℝ} (hadp : Adapted 𝒢 f) (hint : ∀ (i : ℕ), Integrable (f i) μ) (hf : ∀ (i : ℕ), f i =ᶠ[ae μ] μ[f (i + 1)|↑𝒢 i]) :

Martingale f 𝒢 μ

theorem MeasureTheory.submartingale_of_condExp_sub_nonneg_nat {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : Measure Ω} {𝒢 : Filtration ℕ m0} [IsFiniteMeasure μ] {f : ℕ → Ω → ℝ} (hadp : Adapted 𝒢 f) (hint : ∀ (i : ℕ), Integrable (f i) μ) (hf : ∀ (i : ℕ), 0 ≤ᶠ[ae μ] μ[f (i + 1) - f i|↑𝒢 i]) :

Submartingale f 𝒢 μ

theorem MeasureTheory.supermartingale_of_condExp_sub_nonneg_nat {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : Measure Ω} {𝒢 : Filtration ℕ m0} [IsFiniteMeasure μ] {f : ℕ → Ω → ℝ} (hadp : Adapted 𝒢 f) (hint : ∀ (i : ℕ), Integrable (f i) μ) (hf : ∀ (i : ℕ), 0 ≤ᶠ[ae μ] μ[f i - f (i + 1)|↑𝒢 i]) :

Supermartingale f 𝒢 μ

theorem MeasureTheory.martingale_of_condExp_sub_eq_zero_nat {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : Measure Ω} {𝒢 : Filtration ℕ m0} [IsFiniteMeasure μ] {f : ℕ → Ω → ℝ} (hadp : Adapted 𝒢 f) (hint : ∀ (i : ℕ), Integrable (f i) μ) (hf : ∀ (i : ℕ), μ[f (i + 1) - f i|↑𝒢 i] =ᶠ[ae μ] 0) :

Martingale f 𝒢 μ

theorem MeasureTheory.Submartingale.zero_le_of_predictable {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {𝒢 : Filtration ℕ m0} [Preorder E] [SigmaFiniteFiltration μ 𝒢] {f : ℕ → Ω → E} (hfmgle : Submartingale f 𝒢 μ) (hfadp : Adapted 𝒢 fun (n : ℕ) => f (n + 1)) (n : ℕ) :

f 0 ≤ᶠ[ae μ] 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 Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {𝒢 : Filtration ℕ m0} [Preorder E] [SigmaFiniteFiltration μ 𝒢] {f : ℕ → Ω → E} (hfmgle : Supermartingale f 𝒢 μ) (hfadp : Adapted 𝒢 fun (n : ℕ) => f (n + 1)) (n : ℕ) :

f n ≤ᶠ[ae μ] 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 Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {𝒢 : Filtration ℕ m0} [SigmaFiniteFiltration μ 𝒢] {f : ℕ → Ω → E} (hfmgle : Martingale f 𝒢 μ) (hfadp : Adapted 𝒢 fun (n : ℕ) => f (n + 1)) (n : ℕ) :

f n =ᶠ[ae μ] 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 Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {𝒢 : Filtration ℕ m0} [LE E] {f : ℕ → Ω → E} (hf : Submartingale f 𝒢 μ) {τ : Ω → ℕ} (hτ : IsStoppingTime 𝒢 τ) {N : ℕ} (hbdd : ∀ (ω : Ω), τ ω ≤ N) :

Integrable (stoppedValue f τ) μ

theorem MeasureTheory.Submartingale.sum_mul_sub {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : Measure Ω} {𝒢 : Filtration ℕ m0} [IsFiniteMeasure μ] {R : ℝ} {ξ f : ℕ → Ω → ℝ} (hf : Submartingale f 𝒢 μ) (hξ : Adapted 𝒢 ξ) (hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R) (hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω) :

Submartingale (fun (n : ℕ) => ∑ k ∈ Finset.range n, ξ k * (f (k + 1) - f k)) 𝒢 μ

theorem MeasureTheory.Submartingale.sum_mul_sub' {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : Measure Ω} {𝒢 : Filtration ℕ m0} [IsFiniteMeasure μ] {R : ℝ} {ξ f : ℕ → Ω → ℝ} (hf : Submartingale f 𝒢 μ) (hξ : Adapted 𝒢 fun (n : ℕ) => ξ (n + 1)) (hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R) (hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω) :

Submartingale (fun (n : ℕ) => ∑ k ∈ Finset.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.