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 ℱ μ:fis a martingale with respect to filtrationℱand measureμ.measure_theory.supermartingale f ℱ μ:fis a supermartingale with respect to filtrationℱand measureμ.measure_theory.submartingale f ℱ μ:fis 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_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
- measure_theory.martingale f ℱ μ = (measure_theory.adapted ℱ f ∧ ∀ (i j : ι), i ≤ j → measure_theory.condexp (⇑ℱ i) μ (f j) =ᵐ[μ] f i)
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
- measure_theory.supermartingale f ℱ μ = (measure_theory.adapted ℱ f ∧ (∀ (i j : ι), i ≤ j → measure_theory.condexp (⇑ℱ i) μ (f j) ≤ᵐ[μ] f i) ∧ ∀ (i : ι), measure_theory.integrable (f i) μ)
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
- measure_theory.submartingale f ℱ μ = (measure_theory.adapted ℱ f ∧ (∀ (i j : ι), i ≤ j → f i ≤ᵐ[μ] measure_theory.condexp (⇑ℱ i) μ (f j)) ∧ ∀ (i : ι), measure_theory.integrable (f i) μ)
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 : ι) :
measure_theory.integrable (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) :
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 ℱ μ) :
measure_theory.martingale (f + 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 ℱ μ) :
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 ℱ μ) :
measure_theory.martingale (f - 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 ℱ μ) :
measure_theory.martingale (c • 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] :
measure_theory.martingale f ℱ μ ↔ measure_theory.supermartingale f ℱ μ ∧ measure_theory.submartingale f ℱ μ
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 : ι) :
measure_theory.integrable (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) :
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 ℱ μ) :
measure_theory.supermartingale (f + 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 ℱ μ) :
measure_theory.supermartingale (f + 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 ℱ μ) :
measure_theory.submartingale (-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 : ι) :
measure_theory.integrable (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 ℱ μ) :
measure_theory.submartingale (f + 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 ℱ μ) :
measure_theory.submartingale (f + 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 ℱ μ) :
measure_theory.supermartingale (-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) :
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 ℱ μ) :
measure_theory.submartingale (f - 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 ℱ μ) :
measure_theory.submartingale (f - 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 ℱ μ) :
measure_theory.submartingale (f ⊔ 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 ≤ j → 0 ≤ᵐ[μ] 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 ≤ j → 0 ≤ᵐ[μ] 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 ℱ μ) :
measure_theory.supermartingale (f - 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 ℱ μ) :
measure_theory.supermartingale (f - 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 ℱ μ) :
measure_theory.supermartingale (c • 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 ℱ μ) :
measure_theory.submartingale (c • 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 ℱ μ) :
measure_theory.submartingale (c • 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 ℱ μ) :
measure_theory.supermartingale (c • 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 : ℕ) :
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 : ℕ) :
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 Ω}
[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 : ℕ) :
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.