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

• 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} [] {m0 : } [] [] (f : ιΩE) (ℱ : ) (μ : ) :

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} [] {m0 : } [] [] [LE E] (f : ιΩE) (ℱ : ) (μ : ) :

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} [] {m0 : } [] [] [LE E] (f : ιΩE) (ℱ : ) (μ : ) :

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} [] {m0 : } [] [] (ℱ : ) (μ : ) (x : E) :
MeasureTheory.Martingale (fun (x_1 : ι) (x_2 : Ω) => x) μ
theorem MeasureTheory.martingale_const_fun {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [] {m0 : } [] [] [] (ℱ : ) (μ : ) {f : ΩE} (hf : ) (hfint : ) :
MeasureTheory.Martingale (fun (x : ι) => f) μ
theorem MeasureTheory.martingale_zero {Ω : Type u_1} (E : Type u_2) {ι : Type u_3} [] {m0 : } [] [] (ℱ : ) (μ : ) :
theorem MeasureTheory.Martingale.adapted {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [] {m0 : } {μ : } [] [] {f : ιΩE} {ℱ : } (hf : ) :
theorem MeasureTheory.Martingale.stronglyMeasurable {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [] {m0 : } {μ : } [] [] {f : ιΩE} {ℱ : } (hf : ) (i : ι) :
theorem MeasureTheory.Martingale.condexp_ae_eq {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [] {m0 : } {μ : } [] [] {f : ιΩE} {ℱ : } (hf : ) {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} [] {m0 : } {μ : } [] [] {f : ιΩE} {ℱ : } (hf : ) (i : ι) :
theorem MeasureTheory.Martingale.setIntegral_eq {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [] {m0 : } {μ : } [] [] {f : ιΩE} {ℱ : } (hf : ) {i : ι} {j : ι} (hij : i j) {s : Set Ω} (hs : ) :
∫ (ω : Ω) 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} [] {m0 : } {μ : } [] [] {f : ιΩE} {ℱ : } (hf : ) {i : ι} {j : ι} (hij : i j) {s : Set Ω} (hs : ) :
∫ (ω : Ω) 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} [] {m0 : } {μ : } [] [] {f : ιΩE} {g : ιΩE} {ℱ : } (hf : ) (hg : ) :
theorem MeasureTheory.Martingale.neg {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [] {m0 : } {μ : } [] [] {f : ιΩE} {ℱ : } (hf : ) :
theorem MeasureTheory.Martingale.sub {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [] {m0 : } {μ : } [] [] {f : ιΩE} {g : ιΩE} {ℱ : } (hf : ) (hg : ) :
theorem MeasureTheory.Martingale.smul {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [] {m0 : } {μ : } [] [] {f : ιΩE} {ℱ : } (c : ) (hf : ) :
theorem MeasureTheory.Martingale.supermartingale {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [] {m0 : } {μ : } [] [] {f : ιΩE} {ℱ : } [] (hf : ) :
theorem MeasureTheory.Martingale.submartingale {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [] {m0 : } {μ : } [] [] {f : ιΩE} {ℱ : } [] (hf : ) :
theorem MeasureTheory.martingale_iff {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [] {m0 : } {μ : } [] [] {f : ιΩE} {ℱ : } [] :
theorem MeasureTheory.martingale_condexp {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [] {m0 : } [] [] (f : ΩE) (ℱ : ) (μ : ) :
MeasureTheory.Martingale (fun (i : ι) => MeasureTheory.condexp ( i) μ f) μ
theorem MeasureTheory.Supermartingale.adapted {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [] {m0 : } {μ : } [] [] {f : ιΩE} {ℱ : } [LE E] (hf : ) :
theorem MeasureTheory.Supermartingale.stronglyMeasurable {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [] {m0 : } {μ : } [] [] {f : ιΩE} {ℱ : } [LE E] (hf : ) (i : ι) :
theorem MeasureTheory.Supermartingale.integrable {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [] {m0 : } {μ : } [] [] {f : ιΩE} {ℱ : } [LE E] (hf : ) (i : ι) :
theorem MeasureTheory.Supermartingale.condexp_ae_le {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [] {m0 : } {μ : } [] [] {f : ιΩE} {ℱ : } [LE E] (hf : ) {i : ι} {j : ι} (hij : i j) :
MeasureTheory.condexp ( i) μ (f j) ≤ᵐ[μ] f i
theorem MeasureTheory.Supermartingale.setIntegral_le {Ω : Type u_1} {ι : Type u_3} [] {m0 : } {μ : } {ℱ : } {f : ιΩ} (hf : ) {i : ι} {j : ι} (hij : i j) {s : Set Ω} (hs : ) :
∫ (ω : Ω) 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} [] {m0 : } {μ : } {ℱ : } {f : ιΩ} (hf : ) {i : ι} {j : ι} (hij : i j) {s : Set Ω} (hs : ) :
∫ (ω : Ω) 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} [] {m0 : } {μ : } [] [] {f : ιΩE} {g : ιΩE} {ℱ : } [] [CovariantClass E E (fun (x x_1 : E) => x + x_1) fun (x x_1 : E) => x x_1] (hf : ) (hg : ) :
theorem MeasureTheory.Supermartingale.add_martingale {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [] {m0 : } {μ : } [] [] {f : ιΩE} {g : ιΩE} {ℱ : } [] [CovariantClass E E (fun (x x_1 : E) => x + x_1) fun (x x_1 : E) => x x_1] (hf : ) (hg : ) :
theorem MeasureTheory.Supermartingale.neg {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [] {m0 : } {μ : } [] [] {f : ιΩE} {ℱ : } [] [CovariantClass E E (fun (x x_1 : E) => x + x_1) fun (x x_1 : E) => x x_1] (hf : ) :
theorem MeasureTheory.Submartingale.adapted {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [] {m0 : } {μ : } [] [] {f : ιΩE} {ℱ : } [LE E] (hf : ) :
theorem MeasureTheory.Submartingale.stronglyMeasurable {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [] {m0 : } {μ : } [] [] {f : ιΩE} {ℱ : } [LE E] (hf : ) (i : ι) :
theorem MeasureTheory.Submartingale.integrable {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [] {m0 : } {μ : } [] [] {f : ιΩE} {ℱ : } [LE E] (hf : ) (i : ι) :
theorem MeasureTheory.Submartingale.ae_le_condexp {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [] {m0 : } {μ : } [] [] {f : ιΩE} {ℱ : } [LE E] (hf : ) {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} [] {m0 : } {μ : } [] [] {f : ιΩE} {g : ιΩE} {ℱ : } [] [CovariantClass E E (fun (x x_1 : E) => x + x_1) fun (x x_1 : E) => x x_1] (hf : ) (hg : ) :
theorem MeasureTheory.Submartingale.add_martingale {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [] {m0 : } {μ : } [] [] {f : ιΩE} {g : ιΩE} {ℱ : } [] [CovariantClass E E (fun (x x_1 : E) => x + x_1) fun (x x_1 : E) => x x_1] (hf : ) (hg : ) :
theorem MeasureTheory.Submartingale.neg {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [] {m0 : } {μ : } [] [] {f : ιΩE} {ℱ : } [] [CovariantClass E E (fun (x x_1 : E) => x + x_1) fun (x x_1 : E) => x x_1] (hf : ) :
theorem MeasureTheory.Submartingale.setIntegral_le {Ω : Type u_1} {ι : Type u_3} [] {m0 : } {μ : } {ℱ : } {f : ιΩ} (hf : ) {i : ι} {j : ι} (hij : i j) {s : Set Ω} (hs : ) :
∫ (ω : Ω) 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} [] {m0 : } {μ : } {ℱ : } {f : ιΩ} (hf : ) {i : ι} {j : ι} (hij : i j) {s : Set Ω} (hs : ) :
∫ (ω : Ω) 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} [] {m0 : } {μ : } [] [] {f : ιΩE} {g : ιΩE} {ℱ : } [] [CovariantClass E E (fun (x x_1 : E) => x + x_1) fun (x x_1 : E) => x x_1] (hf : ) (hg : ) :
theorem MeasureTheory.Submartingale.sub_martingale {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [] {m0 : } {μ : } [] [] {f : ιΩE} {g : ιΩE} {ℱ : } [] [CovariantClass E E (fun (x x_1 : E) => x + x_1) fun (x x_1 : E) => x x_1] (hf : ) (hg : ) :
theorem MeasureTheory.Submartingale.sup {Ω : Type u_1} {ι : Type u_3} [] {m0 : } {μ : } {ℱ : } {f : ιΩ} {g : ιΩ} (hf : ) (hg : ) :
theorem MeasureTheory.Submartingale.pos {Ω : Type u_1} {ι : Type u_3} [] {m0 : } {μ : } {ℱ : } {f : ιΩ} (hf : ) :
theorem MeasureTheory.submartingale_of_setIntegral_le {Ω : Type u_1} {ι : Type u_3} [] {m0 : } {μ : } {ℱ : } {f : ιΩ} (hadp : ) (hint : ∀ (i : ι), MeasureTheory.Integrable (f i) μ) (hf : ∀ (i j : ι), i j∀ (s : Set Ω), ∫ (ω : Ω) 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} [] {m0 : } {μ : } {ℱ : } {f : ιΩ} (hadp : ) (hint : ∀ (i : ι), MeasureTheory.Integrable (f i) μ) (hf : ∀ (i j : ι), i j∀ (s : Set Ω), ∫ (ω : Ω) 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} [] {m0 : } {μ : } {ℱ : } {f : ιΩ} (hadp : ) (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} [] {m0 : } {μ : } {ℱ : } {f : ιΩ} (hf : ) {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} [] {m0 : } {μ : } {ℱ : } {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} [] {m0 : } {μ : } [] [] {f : ιΩE} {g : ιΩE} {ℱ : } [] [CovariantClass E E (fun (x x_1 : E) => x + x_1) fun (x x_1 : E) => x x_1] (hf : ) (hg : ) :
theorem MeasureTheory.Supermartingale.sub_martingale {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [] {m0 : } {μ : } [] [] {f : ιΩE} {g : ιΩE} {ℱ : } [] [CovariantClass E E (fun (x x_1 : E) => x + x_1) fun (x x_1 : E) => x x_1] (hf : ) (hg : ) :
theorem MeasureTheory.Supermartingale.smul_nonneg {Ω : Type u_1} {ι : Type u_3} [] {m0 : } {μ : } {ℱ : } {F : Type u_4} [] [] [] {f : ιΩF} {c : } (hc : 0 c) (hf : ) :
theorem MeasureTheory.Supermartingale.smul_nonpos {Ω : Type u_1} {ι : Type u_3} [] {m0 : } {μ : } {ℱ : } {F : Type u_4} [] [] [] {f : ιΩF} {c : } (hc : c 0) (hf : ) :
theorem MeasureTheory.Submartingale.smul_nonneg {Ω : Type u_1} {ι : Type u_3} [] {m0 : } {μ : } {ℱ : } {F : Type u_4} [] [] [] {f : ιΩF} {c : } (hc : 0 c) (hf : ) :
theorem MeasureTheory.Submartingale.smul_nonpos {Ω : Type u_1} {ι : Type u_3} [] {m0 : } {μ : } {ℱ : } {F : Type u_4} [] [] [] {f : ιΩF} {c : } (hc : c 0) (hf : ) :
theorem MeasureTheory.submartingale_of_setIntegral_le_succ {Ω : Type u_1} {m0 : } {μ : } {𝒢 : } {f : Ω} (hadp : ) (hint : ∀ (i : ), MeasureTheory.Integrable (f i) μ) (hf : ∀ (i : ) (s : Set Ω), ∫ (ω : Ω) 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 : } {μ : } {𝒢 : } {f : Ω} (hadp : ) (hint : ∀ (i : ), MeasureTheory.Integrable (f i) μ) (hf : ∀ (i : ) (s : Set Ω), ∫ (ω : Ω) 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 : } {μ : } {𝒢 : } {f : Ω} (hadp : ) (hint : ∀ (i : ), MeasureTheory.Integrable (f i) μ) (hf : ∀ (i : ) (s : Set Ω), ∫ (ω : Ω) 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 : } {μ : } {𝒢 : } {f : Ω} (hadp : ) (hint : ∀ (i : ), MeasureTheory.Integrable (f i) μ) (hf : ∀ (i : ) (s : Set Ω), ∫ (ω : Ω) 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 : } {μ : } {𝒢 : } {f : Ω} (hadp : ) (hint : ∀ (i : ), MeasureTheory.Integrable (f i) μ) (hf : ∀ (i : ) (s : Set Ω), ∫ (ω : Ω) 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 : } {μ : } {𝒢 : } {f : Ω} (hadp : ) (hint : ∀ (i : ), MeasureTheory.Integrable (f i) μ) (hf : ∀ (i : ) (s : Set Ω), ∫ (ω : Ω) 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 : } {μ : } {𝒢 : } {f : Ω} (hadp : ) (hint : ∀ (i : ), MeasureTheory.Integrable (f i) μ) (hf : ∀ (i : ), f i ≤ᵐ[μ] MeasureTheory.condexp (𝒢 i) μ (f (i + 1))) :
theorem MeasureTheory.supermartingale_nat {Ω : Type u_1} {m0 : } {μ : } {𝒢 : } {f : Ω} (hadp : ) (hint : ∀ (i : ), MeasureTheory.Integrable (f i) μ) (hf : ∀ (i : ), MeasureTheory.condexp (𝒢 i) μ (f (i + 1)) ≤ᵐ[μ] f i) :
theorem MeasureTheory.martingale_nat {Ω : Type u_1} {m0 : } {μ : } {𝒢 : } {f : Ω} (hadp : ) (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 : } {μ : } {𝒢 : } {f : Ω} (hadp : ) (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 : } {μ : } {𝒢 : } {f : Ω} (hadp : ) (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 : } {μ : } {𝒢 : } {f : Ω} (hadp : ) (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 : } {μ : } [] [] {𝒢 : } [] {f : ΩE} (hfmgle : ) (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 : } {μ : } [] [] {𝒢 : } [] {f : ΩE} (hfmgle : ) (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 : } {μ : } [] [] {𝒢 : } {f : ΩE} (hfmgle : ) (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 : } {μ : } [] [] {𝒢 : } [LE E] {f : ΩE} (hf : ) {τ : Ω} (hτ : ) {N : } (hbdd : ∀ (ω : Ω), τ ω N) :
theorem MeasureTheory.Submartingale.sum_mul_sub {Ω : Type u_1} {m0 : } {μ : } {𝒢 : } {R : } {ξ : Ω} {f : Ω} (hf : ) (hξ : ) (hbdd : ∀ (n : ) (ω : Ω), ξ n ω R) (hnonneg : ∀ (n : ) (ω : Ω), 0 ξ n ω) :
MeasureTheory.Submartingale (fun (n : ) => k, ξ k * (f (k + 1) - f k)) 𝒢 μ
theorem MeasureTheory.Submartingale.sum_mul_sub' {Ω : Type u_1} {m0 : } {μ : } {𝒢 : } {R : } {ξ : Ω} {f : Ω} (hf : ) (hξ : MeasureTheory.Adapted 𝒢 fun (n : ) => ξ (n + 1)) (hbdd : ∀ (n : ) (ω : Ω), ξ n ω R) (hnonneg : ∀ (n : ) (ω : Ω), 0 ξ n ω) :
MeasureTheory.Submartingale (fun (n : ) => k, ξ (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.