# mathlibdocumentation

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 #

• measure_theory.martingale f ℱ μ: f is a martingale with respect to filtration ℱ and measure μ.
• measure_theory.supermartingale f ℱ μ: f is a supermartingale with respect to filtration ℱ and measure μ.
• measure_theory.submartingale f ℱ μ: f is a submartingale with respect to filtration ℱ and measure μ.

### Results #

• measure_theory.martingale_condexp f ℱ μ: the sequence λ i, μ[f | ℱ i, ℱ.le i]) is a martingale with respect to ℱ and μ.
def measure_theory.martingale {α : Type u_1} {E : Type u_2} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} [normed_group E] [ E] (f : ι → α → E) (ℱ : 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] [ E] [has_le E] (f : ι → α → E) (ℱ : 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] [ E] [has_le E] (f : ι → α → E) (ℱ : 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] [ E] (ℱ : 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] [ E] {f : ι → α → E} {ℱ : m0} (hf : μ) :
@[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] [ E] {f : ι → α → E} {ℱ : m0} (hf : μ) (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] [ E] {f : ι → α → E} {ℱ : m0} (hf : μ) {i j : ι} (hij : i j) :
μ (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] [ E] {f : ι → α → E} {ℱ : m0} (hf : μ) (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] [ E] {f : ι → α → E} {ℱ : m0} (hf : μ) {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] [ E] {f g : ι → α → E} {ℱ : m0} (hf : μ) (hg : μ) :
μ
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] [ E] {f : ι → α → E} {ℱ : m0} (hf : μ) :
μ
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] [ E] {f g : ι → α → E} {ℱ : m0} (hf : μ) (hg : μ) :
μ
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] [ E] {f : ι → α → E} {ℱ : m0} (c : ) (hf : μ) :
μ
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] [ E] {f : ι → α → E} {ℱ : m0} [preorder E] (hf : μ) :
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] [ E] {f : ι → α → E} {ℱ : m0} [preorder E] (hf : μ) :
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] [ E] {f : ι → α → E} {ℱ : m0}  :
theorem measure_theory.martingale_condexp {α : Type u_1} {E : Type u_2} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} [normed_group E] [ E] (f : α → E) (ℱ : m0) (μ : measure_theory.measure α)  :
measure_theory.martingale (λ (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] [ E] {f : ι → α → E} {ℱ : m0} [has_le E] (hf : μ) :
@[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] [ E] {f : ι → α → E} {ℱ : m0} [has_le E] (hf : μ) (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] [ E] {f : ι → α → E} {ℱ : m0} [has_le E] (hf : μ) (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] [ E] {f : ι → α → E} {ℱ : m0} [has_le E] (hf : μ) {i j : ι} (hij : i j) :
μ (f j) ≤ᵐ[μ] f i
theorem measure_theory.supermartingale.set_integral_le {α : Type u_1} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} {μ : measure_theory.measure α} {ℱ : m0} {f : ι → α → } (hf : μ) {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] [ E] {f g : ι → α → E} {ℱ : m0} [preorder E] (hf : μ) (hg : μ) :
μ
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] [ E] {f g : ι → α → E} {ℱ : m0} [preorder E] (hf : μ) (hg : μ) :
μ
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] [ E] {f : ι → α → E} {ℱ : m0} [preorder E] (hf : μ) :
@[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] [ E] {f : ι → α → E} {ℱ : m0} [has_le E] (hf : μ) :
@[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] [ E] {f : ι → α → E} {ℱ : m0} [has_le E] (hf : μ) (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] [ E] {f : ι → α → E} {ℱ : m0} [has_le E] (hf : μ) (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] [ E] {f : ι → α → E} {ℱ : m0} [has_le E] (hf : μ) {i j : ι} (hij : i j) :
f 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] [ E] {f g : ι → α → E} {ℱ : m0} [preorder E] (hf : μ) (hg : μ) :
μ
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] [ E] {f g : ι → α → E} {ℱ : m0} [preorder E] (hf : μ) (hg : μ) :
μ
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] [ E] {f : ι → α → E} {ℱ : m0} [preorder E] (hf : μ) :
theorem measure_theory.submartingale.set_integral_le {α : Type u_1} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} {μ : measure_theory.measure α} {ℱ : m0} {f : ι → α → } (hf : μ) {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] [ E] {f g : ι → α → E} {ℱ : m0} [preorder E] (hf : μ) (hg : μ) :
μ
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] [ E] {f g : ι → α → E} {ℱ : m0} [preorder E] (hf : μ) (hg : μ) :
μ
theorem measure_theory.submartingale_of_set_integral_le {α : Type u_1} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} {μ : measure_theory.measure α} {ℱ : m0} {f : ι → α → } (hadp : f) (hint : ∀ (i : ι), μ) (hf : ∀ (i j : ι), i j∀ (s : set α), (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 α} {ℱ : m0} {f : ι → α → } (hadp : f) (hint : ∀ (i : ι), μ) (hf : ∀ (i j : ι), i j0 ≤ᵐ[μ] μ (f j - f i)) :
theorem measure_theory.submartingale.condexp_sub_nonneg {α : Type u_1} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} {μ : measure_theory.measure α} {ℱ : m0} {f : ι → α → } (hf : μ) {i j : ι} (hij : i j) :
0 ≤ᵐ[μ] μ (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 α} {ℱ : m0} {f : ι → α → } :
(∀ (i : ι), μ) ∀ (i j : ι), i j0 ≤ᵐ[μ] μ (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] [ E] {f g : ι → α → E} {ℱ : m0} [preorder E] (hf : μ) (hg : μ) :
μ
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] [ E] {f g : ι → α → E} {ℱ : m0} [preorder E] (hf : μ) (hg : μ) :
μ
theorem measure_theory.supermartingale.smul_nonneg {α : Type u_1} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} {μ : measure_theory.measure α} {ℱ : m0} {F : Type u_4} [ F] [ F] {f : ι → α → F} {c : } (hc : 0 c) (hf : μ) :
μ
theorem measure_theory.supermartingale.smul_nonpos {α : Type u_1} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} {μ : measure_theory.measure α} {ℱ : m0} {F : Type u_4} [ F] [ F] {f : ι → α → F} {c : } (hc : c 0) (hf : μ) :
μ
theorem measure_theory.submartingale.smul_nonneg {α : Type u_1} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} {μ : measure_theory.measure α} {ℱ : m0} {F : Type u_4} [ F] [ F] {f : ι → α → F} {c : } (hc : 0 c) (hf : μ) :
μ
theorem measure_theory.submartingale.smul_nonpos {α : Type u_1} {ι : Type u_3} [preorder ι] {m0 : measurable_space α} {μ : measure_theory.measure α} {ℱ : m0} {F : Type u_4} [ F] [ F] {f : ι → α → F} {c : } (hc : c 0) (hf : μ) :
μ
theorem measure_theory.submartingale_of_set_integral_le_succ {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {𝒢 : m0} {f : α → } (hadp : f) (hint : ∀ (i : ), μ) (hf : ∀ (i : ) (s : set α), (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 α} {𝒢 : m0} {f : α → } (hadp : f) (hint : ∀ (i : ), μ) (hf : ∀ (i : ), f i ≤ᵐ[μ] μ (f (i + 1))) :
theorem measure_theory.submartingale_of_condexp_sub_nonneg_nat {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {𝒢 : m0} {f : α → } (hadp : f) (hint : ∀ (i : ), μ) (hf : ∀ (i : ), 0 ≤ᵐ[μ] μ (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] [ E] {𝒢 : m0} [has_le E] {f : α → E} (hf : μ) {τ : α → } (hτ : τ) {N : } (hbdd : ∀ (x : α), τ x N) :
theorem measure_theory.submartingale.expected_stopped_value_mono {α : Type u_1} {m0 : measurable_space α} {μ : measure_theory.measure α} {𝒢 : m0} {f : α → } (hf : μ) {τ π : α → } (hτ : τ) (hπ : π) (hle : τ π) {N : } (hbdd : ∀ (x : α), π x N) :
(x : α), μ (x : α), μ

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 α} {𝒢 : m0} {f : α → } (hadp : f) (hint : ∀ (i : ), μ) (hf : ∀ (τ π : α → ), τ π(∃ (N : ), ∀ (x : α), π x N) (x : α), μ (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 α} {𝒢 : m0} {f : α → } (hadp : f) (hint : ∀ (i : ), μ) :
∀ (τ π : α → ), τ π(∃ (N : ), ∀ (x : α), π x N) (x : α), μ (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 π.