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 #
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 ι]
[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
- measure_theory.martingale f ℱ μ = (measure_theory.adapted ℱ f ∧ ∀ (i j : ι), i ≤ j → μ[f j|_] =ᵐ[μ] f i)
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
- measure_theory.supermartingale f ℱ μ = (measure_theory.adapted ℱ f ∧ (∀ (i j : ι), i ≤ j → μ[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 ι]
[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
- measure_theory.submartingale f ℱ μ = (measure_theory.adapted ℱ f ∧ (∀ (i j : ι), i ≤ j → f i ≤ᵐ[μ] (μ[f j|_])) ∧ ∀ (i : ι), measure_theory.integrable (f i) μ)
theorem
measure_theory.martingale_zero
{α : 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]
(ℱ : measure_theory.filtration ι m0)
(μ : measure_theory.measure α)
[measure_theory.sigma_finite_filtration μ ℱ] :
@[protected]
theorem
measure_theory.martingale.adapted
{α : 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 ℱ μ) :
@[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 : ι) :
measurable (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) :
@[protected]
theorem
measure_theory.martingale.integrable
{α : 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 : ι) :
measure_theory.integrable (f i) μ
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) :
theorem
measure_theory.martingale.add
{α : 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 g : ι → α → E}
{ℱ : measure_theory.filtration ι m0}
[measure_theory.sigma_finite_filtration μ ℱ]
(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 ι]
[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 ℱ μ) :
measure_theory.martingale (-f) ℱ μ
theorem
measure_theory.martingale.sub
{α : 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 g : ι → α → E}
{ℱ : measure_theory.filtration ι m0}
[measure_theory.sigma_finite_filtration μ ℱ]
(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 ι]
[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 μ ℱ]
(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 ι]
[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 μ ℱ]
[preorder E]
(hf : measure_theory.martingale f ℱ μ) :
theorem
measure_theory.martingale.submartingale
{α : 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 μ ℱ]
[preorder E]
(hf : measure_theory.martingale f ℱ μ) :
theorem
measure_theory.martingale_iff
{α : 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 μ ℱ]
[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 ι]
[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 μ ℱ] :
measure_theory.martingale (λ (i : ι), μ[f|_]) ℱ μ
@[protected]
theorem
measure_theory.supermartingale.adapted
{α : 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 ℱ μ) :
@[protected]
theorem
measure_theory.supermartingale.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.supermartingale f ℱ μ)
(i : ι) :
measurable (f i)
@[protected]
theorem
measure_theory.supermartingale.integrable
{α : 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 : ι) :
measure_theory.integrable (f i) μ
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) :
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 ι]
[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 g : ι → α → E}
{ℱ : measure_theory.filtration ι m0}
[measure_theory.sigma_finite_filtration μ ℱ]
[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 ι]
[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 g : ι → α → E}
{ℱ : measure_theory.filtration ι m0}
[measure_theory.sigma_finite_filtration μ ℱ]
[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 ι]
[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 μ ℱ]
[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 ι]
[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 ℱ μ) :
@[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 : ι) :
measurable (f i)
@[protected]
theorem
measure_theory.submartingale.integrable
{α : 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 : ι) :
measure_theory.integrable (f i) μ
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) :
theorem
measure_theory.submartingale.add
{α : 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 g : ι → α → E}
{ℱ : measure_theory.filtration ι m0}
[measure_theory.sigma_finite_filtration μ ℱ]
[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 ι]
[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 g : ι → α → E}
{ℱ : measure_theory.filtration ι m0}
[measure_theory.sigma_finite_filtration μ ℱ]
[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 ι]
[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 μ ℱ]
[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) :
theorem
measure_theory.submartingale.sub_supermartingale
{α : 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 g : ι → α → E}
{ℱ : measure_theory.filtration ι m0}
[measure_theory.sigma_finite_filtration μ ℱ]
[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 ι]
[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 g : ι → α → E}
{ℱ : measure_theory.filtration ι m0}
[measure_theory.sigma_finite_filtration μ ℱ]
[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.supermartingale.sub_submartingale
{α : 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 g : ι → α → E}
{ℱ : measure_theory.filtration ι m0}
[measure_theory.sigma_finite_filtration μ ℱ]
[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 ι]
[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 g : ι → α → E}
{ℱ : measure_theory.filtration ι m0}
[measure_theory.sigma_finite_filtration μ ℱ]
[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}
[measure_theory.sigma_finite_filtration μ ℱ]
{F : Type u_4}
[measurable_space F]
[normed_lattice_add_comm_group F]
[normed_space ℝ F]
[complete_space F]
[borel_space F]
[topological_space.second_countable_topology 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}
[measure_theory.sigma_finite_filtration μ ℱ]
{F : Type u_4}
[measurable_space F]
[normed_lattice_add_comm_group F]
[normed_space ℝ F]
[complete_space F]
[borel_space F]
[topological_space.second_countable_topology 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}
[measure_theory.sigma_finite_filtration μ ℱ]
{F : Type u_4}
[measurable_space F]
[normed_lattice_add_comm_group F]
[normed_space ℝ F]
[complete_space F]
[borel_space F]
[topological_space.second_countable_topology 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}
[measure_theory.sigma_finite_filtration μ ℱ]
{F : Type u_4}
[measurable_space F]
[normed_lattice_add_comm_group F]
[normed_space ℝ F]
[complete_space F]
[borel_space F]
[topological_space.second_countable_topology F]
[ordered_smul ℝ F]
{f : ι → α → F}
{c : ℝ}
(hc : c ≤ 0)
(hf : measure_theory.submartingale f ℱ μ) :
measure_theory.supermartingale (c • f) ℱ μ
theorem
measure_theory.submartingale.integrable_stopped_value
{α : Type u_1}
{E : Type u_2}
[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]
{𝒢 : measure_theory.filtration ℕ m0}
[measure_theory.sigma_finite_filtration μ 𝒢]
[has_le E]
{f : ℕ → α → E}
(hf : measure_theory.submartingale f 𝒢 μ)
{τ : α → ℕ}
(hτ : measure_theory.is_stopping_time 𝒢 τ)
{N : ℕ}
(hbdd : ∀ (x : α), τ x ≤ N) :
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) :
∫ (x : α), measure_theory.stopped_value f τ x ∂μ ≤ ∫ (x : α), measure_theory.stopped_value f π x ∂μ
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.