mathlib3documentation

probability.martingale.basic

Martingales #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 Ω} [ E] (f : ι Ω E) (ℱ : m0) (μ : . "volume_tac") :
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 Ω} [ E] [has_le E] (f : ι Ω E) (ℱ : m0) (μ : . "volume_tac") :
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 Ω} [ E] [has_le E] (f : ι Ω E) (ℱ : m0) (μ : . "volume_tac") :
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_const {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [preorder ι] {m0 : measurable_space Ω} [ E] (ℱ : m0) (μ : measure_theory.measure Ω) (x : E) :
measure_theory.martingale (λ (_x : ι) (_x : Ω), x) μ
theorem measure_theory.martingale_const_fun {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [preorder ι] {m0 : measurable_space Ω} [ E] [order_bot ι] (ℱ : m0) (μ : measure_theory.measure Ω) {f : Ω E} (hfint : μ) :
measure_theory.martingale (λ (_x : ι), f) μ
theorem measure_theory.martingale_zero {Ω : Type u_1} (E : Type u_2) {ι : Type u_3} [preorder ι] {m0 : measurable_space Ω} [ 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 Ω} [ 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 Ω} [ 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 Ω} [ 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 Ω} [ 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 Ω} [ E] {f : ι Ω E} {ℱ : m0} (hf : μ) {i j : ι} (hij : i j) {s : set Ω} (hs : measurable_set s) :
(ω : Ω) in s, f i ω μ = (ω : Ω) in s, f j ω μ
theorem measure_theory.martingale.add {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [preorder ι] {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} [ 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 Ω} [ 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 Ω} [ 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 Ω} [ 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 Ω} [ 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 Ω} [ 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 Ω} [ E] {f : ι Ω E} {ℱ : m0}  :
theorem measure_theory.martingale_condexp {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [preorder ι] {m0 : measurable_space Ω} [ 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 Ω} [ 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 Ω} [ 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 Ω} [ 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 Ω} [ 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) :
(ω : Ω) in s, f j ω μ (ω : Ω) in s, f i ω μ
theorem measure_theory.supermartingale.add {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [preorder ι] {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} [ 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 Ω} [ 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 Ω} [ 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 Ω} [ 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 Ω} [ 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 Ω} [ 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 Ω} [ 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 Ω} [ 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 Ω} [ 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 Ω} [ 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) :
(ω : Ω) in s, f i ω μ (ω : Ω) in s, f j ω μ

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 Ω} [ 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 Ω} [ E] {f g : ι Ω E} {ℱ : m0} [preorder E] (hf : μ) (hg : μ) :
μ
@[protected]
theorem measure_theory.submartingale.sup {Ω : Type u_1} {ι : Type u_3} [preorder ι] {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {ℱ : m0} {f g : ι Ω } (hf : μ) (hg : μ) :
μ
@[protected]
theorem measure_theory.submartingale.pos {Ω : Type u_1} {ι : Type u_3} [preorder ι] {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {ℱ : m0} {f : ι Ω } (hf : μ) :
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 Ω), (ω : Ω) in s, f i ω μ (ω : Ω) in s, f j ω μ) :
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 j 0 ≤ᵐ[μ] μ (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 j 0 ≤ᵐ[μ] μ (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 Ω} [ 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 Ω} [ 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 Ω), (ω : Ω) in s, f i ω μ (ω : Ω) in s, f (i + 1) ω μ) :
theorem measure_theory.supermartingale_of_set_integral_succ_le {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {𝒢 : m0} {f : Ω } (hadp : f) (hint : (i : ), μ) (hf : (i : ) (s : set Ω), (ω : Ω) in s, f (i + 1) ω μ (ω : Ω) in s, f i ω μ) :
theorem measure_theory.martingale_of_set_integral_eq_succ {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {𝒢 : m0} {f : Ω } (hadp : f) (hint : (i : ), μ) (hf : (i : ) (s : set Ω), (ω : Ω) in s, f i ω μ = (ω : Ω) in s, f (i + 1) ω μ) :
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.supermartingale_nat {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {𝒢 : m0} {f : Ω } (hadp : f) (hint : (i : ), μ) (hf : (i : ), μ (f (i + 1)) ≤ᵐ[μ] f i) :
theorem measure_theory.martingale_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.supermartingale_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 - f (i + 1))) :
theorem measure_theory.martingale_of_condexp_sub_eq_zero_nat {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {𝒢 : m0} {f : Ω } (hadp : f) (hint : (i : ), μ) (hf : (i : ), μ (f (i + 1) - f i) =ᵐ[μ] 0) :
theorem measure_theory.submartingale.zero_le_of_predictable {Ω : Type u_1} {E : Type u_2} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} [ E] {𝒢 : m0} [preorder E] {f : Ω E} (hfmgle : μ) (hfadp : (λ (n : ), f (n + 1))) (n : ) :
f 0 ≤ᵐ[μ] f n

A predictable submartingale is a.e. greater equal than its initial state.

theorem measure_theory.supermartingale.le_zero_of_predictable {Ω : Type u_1} {E : Type u_2} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} [ E] {𝒢 : m0} [preorder E] {f : Ω E} (hfmgle : μ) (hfadp : (λ (n : ), f (n + 1))) (n : ) :
f n ≤ᵐ[μ] f 0

A predictable supermartingale is a.e. less equal than its initial state.

theorem measure_theory.martingale.eq_zero_of_predictable {Ω : Type u_1} {E : Type u_2} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} [ E] {𝒢 : m0} {f : Ω E} (hfmgle : μ) (hfadp : (λ (n : ), f (n + 1))) (n : ) :
f n =ᵐ[μ] f 0

A predictable martingale is a.e. equal to its initial state.

@[protected]
theorem measure_theory.submartingale.integrable_stopped_value {Ω : Type u_1} {E : Type u_2} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} [ E] {𝒢 : m0} [has_le E] {f : Ω E} (hf : μ) {τ : Ω } (hτ : τ) {N : } (hbdd : (ω : Ω), τ ω N) :
theorem measure_theory.submartingale.sum_mul_sub {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {𝒢 : m0} {R : } {ξ f : Ω } (hf : μ) (hξ : ξ) (hbdd : (n : ) (ω : Ω), ξ n ω R) (hnonneg : (n : ) (ω : Ω), 0 ξ n ω) :
measure_theory.submartingale (λ (n : ), (finset.range n).sum (λ (k : ), ξ k * (f (k + 1) - f k))) 𝒢 μ
theorem measure_theory.submartingale.sum_mul_sub' {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {𝒢 : m0} {R : } {ξ f : Ω } (hf : μ) (hξ : (λ (n : ), ξ (n + 1))) (hbdd : (n : ) (ω : Ω), ξ n ω R) (hnonneg : (n : ) (ω : Ω), 0 ξ n ω) :
measure_theory.submartingale (λ (n : ), (finset.range n).sum (λ (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 λ n, ∑ k in finset.range n, ξ (k + 1) * (f (k + 1) - f k) is also a submartingale.