mathlib documentation

probability.martingale

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.stopping.

Definitions #

Results #

def measure_theory.martingale {α : Type u_1} {E : Type u_2} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} [normed_group E] [normed_space E] [complete_space E] (f : ι → α → E) (ℱ : measure_theory.filtration ι m0) (μ : measure_theory.measure α) :
Prop

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
def measure_theory.supermartingale {α : Type u_1} {E : Type u_2} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} [normed_group E] [normed_space E] [complete_space E] [has_le E] (f : ι → α → E) (ℱ : measure_theory.filtration ι m0) (μ : measure_theory.measure α) :
Prop

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
def measure_theory.submartingale {α : Type u_1} {E : Type u_2} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} [normed_group E] [normed_space E] [complete_space E] [has_le E] (f : ι → α → E) (ℱ : measure_theory.filtration ι m0) (μ : measure_theory.measure α) :
Prop

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
theorem measure_theory.martingale_zero {α : Type u_1} (E : Type u_2) {ι : Type u_3} [preorder ι] {m0 : measurable_space α} [normed_group E] [normed_space E] [complete_space E] (ℱ : measure_theory.filtration ι m0) (μ : measure_theory.measure α) :
@[protected]
theorem measure_theory.martingale.adapted {α : Type u_1} {E : Type u_2} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group E] [normed_space E] [complete_space E] {f : ι → α → E} {ℱ : measure_theory.filtration ι m0} (hf : measure_theory.martingale f μ) :
@[protected]
theorem measure_theory.martingale.strongly_measurable {α : Type u_1} {E : Type u_2} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group E] [normed_space E] [complete_space E] {f : ι → α → E} {ℱ : measure_theory.filtration ι m0} (hf : measure_theory.martingale f μ) (i : ι) :
theorem measure_theory.martingale.condexp_ae_eq {α : Type u_1} {E : Type u_2} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group E] [normed_space E] [complete_space E] {f : ι → α → E} {ℱ : measure_theory.filtration ι m0} (hf : measure_theory.martingale f μ) {i j : ι} (hij : i j) :
measure_theory.condexp (ℱ i) μ (f j) =ᵐ[μ] f i
@[protected]
theorem measure_theory.martingale.integrable {α : Type u_1} {E : Type u_2} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group E] [normed_space E] [complete_space E] {f : ι → α → E} {ℱ : measure_theory.filtration ι m0} (hf : measure_theory.martingale f μ) (i : ι) :
theorem measure_theory.martingale.set_integral_eq {α : Type u_1} {E : Type u_2} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group E] [normed_space E] [complete_space E] {f : ι → α → E} {ℱ : measure_theory.filtration ι m0} [measure_theory.sigma_finite_filtration μ ℱ] (hf : measure_theory.martingale f μ) {i j : ι} (hij : i j) {s : set α} (hs : measurable_set s) :
(x : α) in s, f i x μ = (x : α) in s, f j x μ
theorem measure_theory.martingale.add {α : Type u_1} {E : Type u_2} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group E] [normed_space E] [complete_space E] {f g : ι → α → E} {ℱ : measure_theory.filtration ι m0} (hf : measure_theory.martingale f μ) (hg : measure_theory.martingale g μ) :
theorem measure_theory.martingale.neg {α : Type u_1} {E : Type u_2} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group E] [normed_space E] [complete_space E] {f : ι → α → E} {ℱ : measure_theory.filtration ι m0} (hf : measure_theory.martingale f μ) :
theorem measure_theory.martingale.sub {α : Type u_1} {E : Type u_2} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group E] [normed_space E] [complete_space E] {f g : ι → α → E} {ℱ : measure_theory.filtration ι m0} (hf : measure_theory.martingale f μ) (hg : measure_theory.martingale g μ) :
theorem measure_theory.martingale.smul {α : Type u_1} {E : Type u_2} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group E] [normed_space E] [complete_space E] {f : ι → α → E} {ℱ : measure_theory.filtration ι m0} (c : ) (hf : measure_theory.martingale f μ) :
theorem measure_theory.martingale.supermartingale {α : Type u_1} {E : Type u_2} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group E] [normed_space E] [complete_space E] {f : ι → α → E} {ℱ : measure_theory.filtration ι m0} [preorder E] (hf : measure_theory.martingale f μ) :
theorem measure_theory.martingale.submartingale {α : Type u_1} {E : Type u_2} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group E] [normed_space E] [complete_space E] {f : ι → α → E} {ℱ : measure_theory.filtration ι m0} [preorder E] (hf : measure_theory.martingale f μ) :
theorem measure_theory.martingale_iff {α : Type u_1} {E : Type u_2} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group E] [normed_space E] [complete_space E] {f : ι → α → E} {ℱ : measure_theory.filtration ι m0} [partial_order E] :
theorem measure_theory.martingale_condexp {α : Type u_1} {E : Type u_2} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} [normed_group E] [normed_space E] [complete_space E] (f : α → E) (ℱ : measure_theory.filtration ι m0) (μ : measure_theory.measure α) [measure_theory.sigma_finite_filtration μ ℱ] :
measure_theory.martingale (λ (i : ι), measure_theory.condexp (ℱ i) μ f) μ
@[protected]
theorem measure_theory.supermartingale.adapted {α : Type u_1} {E : Type u_2} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group E] [normed_space E] [complete_space E] {f : ι → α → E} {ℱ : measure_theory.filtration ι m0} [has_le E] (hf : measure_theory.supermartingale f μ) :
@[protected]
theorem measure_theory.supermartingale.strongly_measurable {α : Type u_1} {E : Type u_2} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group E] [normed_space E] [complete_space E] {f : ι → α → E} {ℱ : measure_theory.filtration ι m0} [has_le E] (hf : measure_theory.supermartingale f μ) (i : ι) :
@[protected]
theorem measure_theory.supermartingale.integrable {α : Type u_1} {E : Type u_2} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group E] [normed_space E] [complete_space E] {f : ι → α → E} {ℱ : measure_theory.filtration ι m0} [has_le E] (hf : measure_theory.supermartingale f μ) (i : ι) :
theorem measure_theory.supermartingale.condexp_ae_le {α : Type u_1} {E : Type u_2} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group E] [normed_space E] [complete_space E] {f : ι → α → E} {ℱ : measure_theory.filtration ι m0} [has_le E] (hf : measure_theory.supermartingale f μ) {i j : ι} (hij : i j) :
measure_theory.condexp (ℱ i) μ (f j) ≤ᵐ[μ] f i
theorem measure_theory.supermartingale.set_integral_le {α : Type u_1} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} {μ : measure_theory.measure α} {ℱ : measure_theory.filtration ι m0} [measure_theory.sigma_finite_filtration μ ℱ] {f : ι → α → } (hf : measure_theory.supermartingale f μ) {i j : ι} (hij : i j) {s : set α} (hs : measurable_set s) :
(x : α) in s, f j x μ (x : α) in s, f i x μ
theorem measure_theory.supermartingale.add {α : Type u_1} {E : Type u_2} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group E] [normed_space E] [complete_space E] {f g : ι → α → E} {ℱ : measure_theory.filtration ι m0} [preorder E] [covariant_class E E has_add.add has_le.le] (hf : measure_theory.supermartingale f μ) (hg : measure_theory.supermartingale g μ) :
theorem measure_theory.supermartingale.add_martingale {α : Type u_1} {E : Type u_2} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group E] [normed_space E] [complete_space E] {f g : ι → α → E} {ℱ : measure_theory.filtration ι m0} [preorder E] [covariant_class E E has_add.add has_le.le] (hf : measure_theory.supermartingale f μ) (hg : measure_theory.martingale g μ) :
theorem measure_theory.supermartingale.neg {α : Type u_1} {E : Type u_2} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group E] [normed_space E] [complete_space E] {f : ι → α → E} {ℱ : measure_theory.filtration ι m0} [preorder E] [covariant_class E E has_add.add has_le.le] (hf : measure_theory.supermartingale f μ) :
@[protected]
theorem measure_theory.submartingale.adapted {α : Type u_1} {E : Type u_2} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group E] [normed_space E] [complete_space E] {f : ι → α → E} {ℱ : measure_theory.filtration ι m0} [has_le E] (hf : measure_theory.submartingale f μ) :
@[protected]
theorem measure_theory.submartingale.strongly_measurable {α : Type u_1} {E : Type u_2} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group E] [normed_space E] [complete_space E] {f : ι → α → E} {ℱ : measure_theory.filtration ι m0} [has_le E] (hf : measure_theory.submartingale f μ) (i : ι) :
@[protected]
theorem measure_theory.submartingale.integrable {α : Type u_1} {E : Type u_2} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group E] [normed_space E] [complete_space E] {f : ι → α → E} {ℱ : measure_theory.filtration ι m0} [has_le E] (hf : measure_theory.submartingale f μ) (i : ι) :
theorem measure_theory.submartingale.ae_le_condexp {α : Type u_1} {E : Type u_2} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group E] [normed_space E] [complete_space E] {f : ι → α → E} {ℱ : measure_theory.filtration ι m0} [has_le E] (hf : measure_theory.submartingale f μ) {i j : ι} (hij : i j) :
f i ≤ᵐ[μ] measure_theory.condexp (ℱ i) μ (f j)
theorem measure_theory.submartingale.add {α : Type u_1} {E : Type u_2} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group E] [normed_space E] [complete_space E] {f g : ι → α → E} {ℱ : measure_theory.filtration ι m0} [preorder E] [covariant_class E E has_add.add has_le.le] (hf : measure_theory.submartingale f μ) (hg : measure_theory.submartingale g μ) :
theorem measure_theory.submartingale.add_martingale {α : Type u_1} {E : Type u_2} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group E] [normed_space E] [complete_space E] {f g : ι → α → E} {ℱ : measure_theory.filtration ι m0} [preorder E] [covariant_class E E has_add.add has_le.le] (hf : measure_theory.submartingale f μ) (hg : measure_theory.martingale g μ) :
theorem measure_theory.submartingale.neg {α : Type u_1} {E : Type u_2} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group E] [normed_space E] [complete_space E] {f : ι → α → E} {ℱ : measure_theory.filtration ι m0} [preorder E] [covariant_class E E has_add.add has_le.le] (hf : measure_theory.submartingale f μ) :
theorem measure_theory.submartingale.set_integral_le {α : Type u_1} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} {μ : measure_theory.measure α} {ℱ : measure_theory.filtration ι m0} [measure_theory.sigma_finite_filtration μ ℱ] {f : ι → α → } (hf : measure_theory.submartingale f μ) {i j : ι} (hij : i j) {s : set α} (hs : measurable_set s) :
(x : α) in s, f i x μ (x : α) in s, f j x μ

The converse of this lemma is measure_theory.submartingale_of_set_integral_le.

theorem measure_theory.submartingale.sub_supermartingale {α : Type u_1} {E : Type u_2} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group E] [normed_space E] [complete_space E] {f g : ι → α → E} {ℱ : measure_theory.filtration ι m0} [preorder E] [covariant_class E E has_add.add has_le.le] (hf : measure_theory.submartingale f μ) (hg : measure_theory.supermartingale g μ) :
theorem measure_theory.submartingale.sub_martingale {α : Type u_1} {E : Type u_2} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group E] [normed_space E] [complete_space E] {f g : ι → α → E} {ℱ : measure_theory.filtration ι m0} [preorder E] [covariant_class E E has_add.add has_le.le] (hf : measure_theory.submartingale f μ) (hg : measure_theory.martingale g μ) :
theorem measure_theory.submartingale_of_set_integral_le {α : Type u_1} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} {μ : measure_theory.measure α} {ℱ : measure_theory.filtration ι m0} [measure_theory.is_finite_measure μ] {f : ι → α → } (hadp : measure_theory.adapted f) (hint : ∀ (i : ι), measure_theory.integrable (f i) μ) (hf : ∀ (i j : ι), i j∀ (s : set α), measurable_set s (x : α) in s, f i x μ (x : α) in s, f j x μ) :
theorem measure_theory.submartingale_of_condexp_sub_nonneg {α : Type u_1} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} {μ : measure_theory.measure α} {ℱ : measure_theory.filtration ι m0} [measure_theory.is_finite_measure μ] {f : ι → α → } (hadp : measure_theory.adapted f) (hint : ∀ (i : ι), measure_theory.integrable (f i) μ) (hf : ∀ (i j : ι), i j0 ≤ᵐ[μ] measure_theory.condexp (ℱ i) μ (f j - f i)) :
theorem measure_theory.submartingale.condexp_sub_nonneg {α : Type u_1} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} {μ : measure_theory.measure α} {ℱ : measure_theory.filtration ι m0} [measure_theory.is_finite_measure μ] {f : ι → α → } (hf : measure_theory.submartingale f μ) {i j : ι} (hij : i j) :
0 ≤ᵐ[μ] measure_theory.condexp (ℱ i) μ (f j - f i)
theorem measure_theory.submartingale_iff_condexp_sub_nonneg {α : Type u_1} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} {μ : measure_theory.measure α} {ℱ : measure_theory.filtration ι m0} [measure_theory.is_finite_measure μ] {f : ι → α → } :
measure_theory.submartingale f μ measure_theory.adapted f (∀ (i : ι), measure_theory.integrable (f i) μ) ∀ (i j : ι), i j0 ≤ᵐ[μ] measure_theory.condexp (ℱ i) μ (f j - f i)
theorem measure_theory.supermartingale.sub_submartingale {α : Type u_1} {E : Type u_2} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group E] [normed_space E] [complete_space E] {f g : ι → α → E} {ℱ : measure_theory.filtration ι m0} [preorder E] [covariant_class E E has_add.add has_le.le] (hf : measure_theory.supermartingale f μ) (hg : measure_theory.submartingale g μ) :
theorem measure_theory.supermartingale.sub_martingale {α : Type u_1} {E : Type u_2} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group E] [normed_space E] [complete_space E] {f g : ι → α → E} {ℱ : measure_theory.filtration ι m0} [preorder E] [covariant_class E E has_add.add has_le.le] (hf : measure_theory.supermartingale f μ) (hg : measure_theory.martingale g μ) :
theorem measure_theory.supermartingale.smul_nonneg {α : Type u_1} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} {μ : measure_theory.measure α} {ℱ : measure_theory.filtration ι m0} {F : Type u_4} [normed_lattice_add_comm_group F] [normed_space F] [complete_space F] [ordered_smul F] {f : ι → α → F} {c : } (hc : 0 c) (hf : measure_theory.supermartingale f μ) :
theorem measure_theory.supermartingale.smul_nonpos {α : Type u_1} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} {μ : measure_theory.measure α} {ℱ : measure_theory.filtration ι m0} {F : Type u_4} [normed_lattice_add_comm_group F] [normed_space F] [complete_space F] [ordered_smul F] {f : ι → α → F} {c : } (hc : c 0) (hf : measure_theory.supermartingale f μ) :
theorem measure_theory.submartingale.smul_nonneg {α : Type u_1} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} {μ : measure_theory.measure α} {ℱ : measure_theory.filtration ι m0} {F : Type u_4} [normed_lattice_add_comm_group F] [normed_space F] [complete_space F] [ordered_smul F] {f : ι → α → F} {c : } (hc : 0 c) (hf : measure_theory.submartingale f μ) :
theorem measure_theory.submartingale.smul_nonpos {α : Type u_1} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} {μ : measure_theory.measure α} {ℱ : measure_theory.filtration ι m0} {F : Type u_4} [normed_lattice_add_comm_group F] [normed_space F] [complete_space F] [ordered_smul F] {f : ι → α → F} {c : } (hc : c 0) (hf : measure_theory.submartingale f μ) :
theorem measure_theory.submartingale_of_set_integral_le_succ {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {𝒢 : measure_theory.filtration m0} [measure_theory.is_finite_measure μ] {f : α → } (hadp : measure_theory.adapted 𝒢 f) (hint : ∀ (i : ), measure_theory.integrable (f i) μ) (hf : ∀ (i : ) (s : set α), measurable_set s (x : α) in s, f i x μ (x : α) in s, f (i + 1) x μ) :
theorem measure_theory.submartingale_nat {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {𝒢 : measure_theory.filtration m0} [measure_theory.is_finite_measure μ] {f : α → } (hadp : measure_theory.adapted 𝒢 f) (hint : ∀ (i : ), measure_theory.integrable (f i) μ) (hf : ∀ (i : ), f i ≤ᵐ[μ] measure_theory.condexp (𝒢 i) μ (f (i + 1))) :
theorem measure_theory.submartingale_of_condexp_sub_nonneg_nat {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {𝒢 : measure_theory.filtration m0} [measure_theory.is_finite_measure μ] {f : α → } (hadp : measure_theory.adapted 𝒢 f) (hint : ∀ (i : ), measure_theory.integrable (f i) μ) (hf : ∀ (i : ), 0 ≤ᵐ[μ] measure_theory.condexp (𝒢 i) μ (f (i + 1) - f i)) :
theorem measure_theory.submartingale.integrable_stopped_value {α : Type u_1} {E : Type u_2} {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group E] [normed_space E] [complete_space E] {𝒢 : measure_theory.filtration m0} [has_le E] {f : α → E} (hf : measure_theory.submartingale f 𝒢 μ) {τ : α → } (hτ : measure_theory.is_stopping_time 𝒢 τ) {N : } (hbdd : ∀ (x : α), τ x N) :
theorem measure_theory.submartingale.expected_stopped_value_mono {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {𝒢 : measure_theory.filtration m0} [measure_theory.sigma_finite_filtration μ 𝒢] {f : α → } (hf : measure_theory.submartingale f 𝒢 μ) {τ π : α → } (hτ : measure_theory.is_stopping_time 𝒢 τ) (hπ : measure_theory.is_stopping_time 𝒢 π) (hle : τ π) {N : } (hbdd : ∀ (x : α), π x N) :

Given a submartingale f and bounded stopping times τ and π such that τ ≤ π, the expectation of stopped_value f τ is less than or equal to the expectation of stopped_value f π. This is the forward direction of the optional stopping theorem.

theorem measure_theory.submartingale_of_expected_stopped_value_mono {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {𝒢 : measure_theory.filtration m0} [measure_theory.is_finite_measure μ] {f : α → } (hadp : measure_theory.adapted 𝒢 f) (hint : ∀ (i : ), measure_theory.integrable (f i) μ) (hf : ∀ (τ π : α → ), measure_theory.is_stopping_time 𝒢 τmeasure_theory.is_stopping_time 𝒢 πτ π(∃ (N : ), ∀ (x : α), π x N) (x : α), measure_theory.stopped_value f τ x μ (x : α), measure_theory.stopped_value f π x μ) :

The converse direction of the optional stopping theorem, i.e. an adapted integrable process f is a submartingale if for all bounded stopping times τ and π such that τ ≤ π, the stopped value of f at τ has expectation smaller than its stopped value at π.

theorem measure_theory.submartingale_iff_expected_stopped_value_mono {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {𝒢 : measure_theory.filtration m0} [measure_theory.is_finite_measure μ] {f : α → } (hadp : measure_theory.adapted 𝒢 f) (hint : ∀ (i : ), measure_theory.integrable (f i) μ) :
measure_theory.submartingale f 𝒢 μ ∀ (τ π : α → ), measure_theory.is_stopping_time 𝒢 τmeasure_theory.is_stopping_time 𝒢 πτ π(∃ (N : ), ∀ (x : α), π x N) (x : α), measure_theory.stopped_value f τ x μ (x : α), measure_theory.stopped_value f π x μ

The optional stopping theorem (fair game theorem): an adapted integrable process f is a submartingale if and only if for all bounded stopping times τ and π such that τ ≤ π, the stopped value of f at τ has expectation smaller than its stopped value at π.