mathlib documentation

probability_theory.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 | ℱ.le 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 | ℱ.le 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 | ℱ.le i].

The definitions of filtration and adapted can be found in probability_theory.stopping.

Definitions #

Results #

def measure_theory.martingale {α : Type u_1} {E : Type u_2} {ι : Type u_3} [preorder ι] [measurable_space E] {m0 : measurable_space α} [normed_group E] [normed_space E] [complete_space E] [borel_space E] [topological_space.second_countable_topology E] (f : ι → α → E) (ℱ : measure_theory.filtration ι m0) (μ : measure_theory.measure α) [measure_theory.sigma_finite_filtration μ ℱ] :
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 | ℱ.le i] =ᵐ[μ] f i.

Equations
def measure_theory.supermartingale {α : Type u_1} {E : Type u_2} {ι : Type u_3} [preorder ι] [measurable_space E] {m0 : measurable_space α} [normed_group E] [normed_space E] [complete_space E] [borel_space E] [topological_space.second_countable_topology E] [has_le E] (f : ι → α → E) (ℱ : measure_theory.filtration ι m0) (μ : measure_theory.measure α) [measure_theory.sigma_finite_filtration μ ℱ] :
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 ι] [measurable_space E] {m0 : measurable_space α} [normed_group E] [normed_space E] [complete_space E] [borel_space E] [topological_space.second_countable_topology E] [has_le E] (f : ι → α → E) (ℱ : measure_theory.filtration ι m0) (μ : measure_theory.measure α) [measure_theory.sigma_finite_filtration μ ℱ] :
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
@[protected]
@[protected]
theorem measure_theory.martingale.measurable {α : Type u_1} {E : Type u_2} {ι : Type u_3} [preorder ι] [measurable_space E] {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group E] [normed_space E] [complete_space E] [borel_space E] [topological_space.second_countable_topology E] {f : ι → α → E} {ℱ : measure_theory.filtration ι m0} [measure_theory.sigma_finite_filtration μ ℱ] (hf : measure_theory.martingale f μ) (i : ι) :
theorem measure_theory.martingale.condexp_ae_eq {α : Type u_1} {E : Type u_2} {ι : Type u_3} [preorder ι] [measurable_space E] {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group E] [normed_space E] [complete_space E] [borel_space E] [topological_space.second_countable_topology E] {f : ι → α → E} {ℱ : measure_theory.filtration ι m0} [measure_theory.sigma_finite_filtration μ ℱ] (hf : measure_theory.martingale f μ) {i j : ι} (hij : i j) :
μ[f j|_] =ᵐ[μ] f i
@[protected]
theorem measure_theory.martingale.set_integral_eq {α : Type u_1} {E : Type u_2} {ι : Type u_3} [preorder ι] [measurable_space E] {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group E] [normed_space E] [complete_space E] [borel_space E] [topological_space.second_countable_topology 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 μ
@[protected]
@[protected]
theorem measure_theory.supermartingale.condexp_ae_le {α : Type u_1} {E : Type u_2} {ι : Type u_3} [preorder ι] [measurable_space E] {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group E] [normed_space E] [complete_space E] [borel_space E] [topological_space.second_countable_topology E] {f : ι → α → E} {ℱ : measure_theory.filtration ι m0} [measure_theory.sigma_finite_filtration μ ℱ] [has_le E] (hf : measure_theory.supermartingale f μ) {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 α} {ℱ : 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 μ
@[protected]
theorem measure_theory.submartingale.measurable {α : Type u_1} {E : Type u_2} {ι : Type u_3} [preorder ι] [measurable_space E] {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group E] [normed_space E] [complete_space E] [borel_space E] [topological_space.second_countable_topology E] {f : ι → α → E} {ℱ : measure_theory.filtration ι m0} [measure_theory.sigma_finite_filtration μ ℱ] [has_le E] (hf : measure_theory.submartingale f μ) (i : ι) :
@[protected]
theorem measure_theory.submartingale.ae_le_condexp {α : Type u_1} {E : Type u_2} {ι : Type u_3} [preorder ι] [measurable_space E] {m0 : measurable_space α} {μ : measure_theory.measure α} [normed_group E] [normed_space E] [complete_space E] [borel_space E] [topological_space.second_countable_topology E] {f : ι → α → E} {ℱ : measure_theory.filtration ι m0} [measure_theory.sigma_finite_filtration μ ℱ] [has_le E] (hf : measure_theory.submartingale f μ) {i j : ι} (hij : i j) :
f i ≤ᵐ[μ] [f j|_])
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 μ
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 or equal to the expectation of stopped_value f π. This is the forward direction of the optional stopping theorem.