mathlib documentation

probability.martingale.basic

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_add_comm_group E] [normed_space E] [complete_space E] (f : ι → Ω → E) (ℱ : measure_theory.filtration ι m0) (μ : measure_theory.measure Ω . "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 Ω} [normed_add_comm_group E] [normed_space E] [complete_space E] [has_le E] (f : ι → Ω → E) (ℱ : measure_theory.filtration ι m0) (μ : measure_theory.measure Ω . "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 Ω} [normed_add_comm_group E] [normed_space E] [complete_space E] [has_le E] (f : ι → Ω → E) (ℱ : measure_theory.filtration ι m0) (μ : measure_theory.measure Ω . "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 Ω} [normed_add_comm_group E] [normed_space E] [complete_space E] (ℱ : measure_theory.filtration ι m0) (μ : measure_theory.measure Ω) [measure_theory.is_finite_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 Ω} [normed_add_comm_group E] [normed_space E] [complete_space E] [order_bot ι] (ℱ : measure_theory.filtration ι m0) (μ : measure_theory.measure Ω) [measure_theory.is_finite_measure μ] {f : Ω → E} (hf : measure_theory.strongly_measurable f) (hfint : measure_theory.integrable f μ) :
measure_theory.martingale (λ (_x : ι), f) μ
theorem measure_theory.martingale_zero {Ω : Type u_1} (E : Type u_2) {ι : Type u_3} [preorder ι] {m0 : measurable_space Ω} [normed_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_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) :
(ω : Ω) 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 Ω} [normed_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_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) :
(ω : Ω) 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 Ω} [normed_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_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_add_comm_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) :
(ω : Ω) 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 Ω} [normed_add_comm_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_add_comm_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 μ) :
@[protected]
theorem measure_theory.submartingale.sup {Ω : Type u_1} {ι : Type u_3} [preorder ι] {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {ℱ : measure_theory.filtration ι m0} {f g : ι → Ω → } (hf : measure_theory.submartingale f μ) (hg : measure_theory.submartingale g μ) :
@[protected]
theorem measure_theory.submartingale.pos {Ω : Type u_1} {ι : Type u_3} [preorder ι] {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {ℱ : measure_theory.filtration ι m0} {f : ι → Ω → } (hf : measure_theory.submartingale f μ) :
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 (ω : Ω) 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 Ω} {ℱ : 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} {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_add_comm_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_add_comm_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 (ω : Ω) 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 Ω} {𝒢 : 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 (ω : Ω) 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 Ω} {𝒢 : 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 (ω : Ω) in s, f i ω μ = (ω : Ω) in s, f (i + 1) ω μ) :
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.supermartingale_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 : ), measure_theory.condexp (𝒢 i) μ (f (i + 1)) ≤ᵐ[μ] f i) :
theorem measure_theory.martingale_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.supermartingale_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 - f (i + 1))) :
theorem measure_theory.martingale_of_condexp_sub_eq_zero_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 : ), measure_theory.condexp (𝒢 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 Ω} [normed_add_comm_group E] [normed_space E] [complete_space E] {𝒢 : measure_theory.filtration m0} [preorder E] [measure_theory.sigma_finite_filtration μ 𝒢] {f : Ω → E} (hfmgle : measure_theory.submartingale f 𝒢 μ) (hfadp : measure_theory.adapted 𝒢 (λ (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 Ω} [normed_add_comm_group E] [normed_space E] [complete_space E] {𝒢 : measure_theory.filtration m0} [preorder E] [measure_theory.sigma_finite_filtration μ 𝒢] {f : Ω → E} (hfmgle : measure_theory.supermartingale f 𝒢 μ) (hfadp : measure_theory.adapted 𝒢 (λ (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_predicatable {Ω : Type u_1} {E : Type u_2} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} [normed_add_comm_group E] [normed_space E] [complete_space E] {𝒢 : measure_theory.filtration m0} [measure_theory.sigma_finite_filtration μ 𝒢] {f : Ω → E} (hfmgle : measure_theory.martingale f 𝒢 μ) (hfadp : measure_theory.adapted 𝒢 (λ (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 Ω} [normed_add_comm_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 : ∀ (ω : Ω), τ ω N) :
theorem measure_theory.submartingale.sum_mul_sub {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {𝒢 : measure_theory.filtration m0} [measure_theory.is_finite_measure μ] {R : } {ξ f : Ω → } (hf : measure_theory.submartingale f 𝒢 μ) (hξ : measure_theory.adapted 𝒢 ξ) (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 Ω} {𝒢 : measure_theory.filtration m0} [measure_theory.is_finite_measure μ] {R : } {ξ f : Ω → } (hf : measure_theory.submartingale f 𝒢 μ) (hξ : measure_theory.adapted 𝒢 (λ (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.