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.Process.Stopping.
Definitions #
MeasureTheory.Martingale f ℱ μ:fis a martingale with respect to filtrationℱand measureμ.MeasureTheory.Supermartingale f ℱ μ:fis a supermartingale with respect to filtrationℱand measureμ.MeasureTheory.Submartingale f ℱ μ:fis a submartingale with respect to filtrationℱand measureμ.
Results #
MeasureTheory.martingale_condexp f ℱ μ: the sequencefun i => μ[f | ℱ i, ℱ.le i])is a martingale with respect toℱandμ.
def
MeasureTheory.Martingale
{Ω : Type u_1}
{E : Type u_2}
{ι : Type u_3}
[Preorder ι]
{m0 : MeasurableSpace Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
(f : ι → Ω → E)
(ℱ : MeasureTheory.Filtration ι m0)
(μ : MeasureTheory.Measure Ω)
:
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
- MeasureTheory.Martingale f ℱ μ = (MeasureTheory.Adapted ℱ f ∧ ∀ (i j : ι), i ≤ j → MeasureTheory.condexp (↑ℱ i) μ (f j) =ᶠ[MeasureTheory.Measure.ae μ] f i)
Instances For
def
MeasureTheory.Supermartingale
{Ω : Type u_1}
{E : Type u_2}
{ι : Type u_3}
[Preorder ι]
{m0 : MeasurableSpace Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
[LE E]
(f : ι → Ω → E)
(ℱ : MeasureTheory.Filtration ι m0)
(μ : MeasureTheory.Measure Ω)
:
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
- One or more equations did not get rendered due to their size.
Instances For
def
MeasureTheory.Submartingale
{Ω : Type u_1}
{E : Type u_2}
{ι : Type u_3}
[Preorder ι]
{m0 : MeasurableSpace Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
[LE E]
(f : ι → Ω → E)
(ℱ : MeasureTheory.Filtration ι m0)
(μ : MeasureTheory.Measure Ω)
:
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
- One or more equations did not get rendered due to their size.
Instances For
theorem
MeasureTheory.martingale_const
{Ω : Type u_1}
{E : Type u_2}
{ι : Type u_3}
[Preorder ι]
{m0 : MeasurableSpace Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
(ℱ : MeasureTheory.Filtration ι m0)
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsFiniteMeasure μ]
(x : E)
:
MeasureTheory.Martingale (fun (x_1 : ι) (x_2 : Ω) => x) ℱ μ
theorem
MeasureTheory.martingale_const_fun
{Ω : Type u_1}
{E : Type u_2}
{ι : Type u_3}
[Preorder ι]
{m0 : MeasurableSpace Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
[OrderBot ι]
(ℱ : MeasureTheory.Filtration ι m0)
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsFiniteMeasure μ]
{f : Ω → E}
(hf : MeasureTheory.StronglyMeasurable f)
(hfint : MeasureTheory.Integrable f)
:
MeasureTheory.Martingale (fun (x : ι) => f) ℱ μ
theorem
MeasureTheory.martingale_zero
{Ω : Type u_1}
(E : Type u_2)
{ι : Type u_3}
[Preorder ι]
{m0 : MeasurableSpace Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
(ℱ : MeasureTheory.Filtration ι m0)
(μ : MeasureTheory.Measure Ω)
:
MeasureTheory.Martingale 0 ℱ μ
theorem
MeasureTheory.Martingale.adapted
{Ω : Type u_1}
{E : Type u_2}
{ι : Type u_3}
[Preorder ι]
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{f : ι → Ω → E}
{ℱ : MeasureTheory.Filtration ι m0}
(hf : MeasureTheory.Martingale f ℱ μ)
:
theorem
MeasureTheory.Martingale.stronglyMeasurable
{Ω : Type u_1}
{E : Type u_2}
{ι : Type u_3}
[Preorder ι]
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{f : ι → Ω → E}
{ℱ : MeasureTheory.Filtration ι m0}
(hf : MeasureTheory.Martingale f ℱ μ)
(i : ι)
:
theorem
MeasureTheory.Martingale.condexp_ae_eq
{Ω : Type u_1}
{E : Type u_2}
{ι : Type u_3}
[Preorder ι]
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{f : ι → Ω → E}
{ℱ : MeasureTheory.Filtration ι m0}
(hf : MeasureTheory.Martingale f ℱ μ)
{i : ι}
{j : ι}
(hij : i ≤ j)
:
MeasureTheory.condexp (↑ℱ i) μ (f j) =ᶠ[MeasureTheory.Measure.ae μ] f i
theorem
MeasureTheory.Martingale.integrable
{Ω : Type u_1}
{E : Type u_2}
{ι : Type u_3}
[Preorder ι]
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{f : ι → Ω → E}
{ℱ : MeasureTheory.Filtration ι m0}
(hf : MeasureTheory.Martingale f ℱ μ)
(i : ι)
:
MeasureTheory.Integrable (f i)
theorem
MeasureTheory.Martingale.set_integral_eq
{Ω : Type u_1}
{E : Type u_2}
{ι : Type u_3}
[Preorder ι]
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{f : ι → Ω → E}
{ℱ : MeasureTheory.Filtration ι m0}
[MeasureTheory.SigmaFiniteFiltration μ ℱ]
(hf : MeasureTheory.Martingale f ℱ μ)
{i : ι}
{j : ι}
(hij : i ≤ j)
{s : Set Ω}
(hs : MeasurableSet s)
:
∫ (ω : Ω) in s, f i ω ∂μ = ∫ (ω : Ω) in s, f j ω ∂μ
theorem
MeasureTheory.Martingale.add
{Ω : Type u_1}
{E : Type u_2}
{ι : Type u_3}
[Preorder ι]
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{f : ι → Ω → E}
{g : ι → Ω → E}
{ℱ : MeasureTheory.Filtration ι m0}
(hf : MeasureTheory.Martingale f ℱ μ)
(hg : MeasureTheory.Martingale g ℱ μ)
:
MeasureTheory.Martingale (f + g) ℱ μ
theorem
MeasureTheory.Martingale.neg
{Ω : Type u_1}
{E : Type u_2}
{ι : Type u_3}
[Preorder ι]
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{f : ι → Ω → E}
{ℱ : MeasureTheory.Filtration ι m0}
(hf : MeasureTheory.Martingale f ℱ μ)
:
MeasureTheory.Martingale (-f) ℱ μ
theorem
MeasureTheory.Martingale.sub
{Ω : Type u_1}
{E : Type u_2}
{ι : Type u_3}
[Preorder ι]
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{f : ι → Ω → E}
{g : ι → Ω → E}
{ℱ : MeasureTheory.Filtration ι m0}
(hf : MeasureTheory.Martingale f ℱ μ)
(hg : MeasureTheory.Martingale g ℱ μ)
:
MeasureTheory.Martingale (f - g) ℱ μ
theorem
MeasureTheory.Martingale.smul
{Ω : Type u_1}
{E : Type u_2}
{ι : Type u_3}
[Preorder ι]
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{f : ι → Ω → E}
{ℱ : MeasureTheory.Filtration ι m0}
(c : ℝ)
(hf : MeasureTheory.Martingale f ℱ μ)
:
MeasureTheory.Martingale (c • f) ℱ μ
theorem
MeasureTheory.Martingale.supermartingale
{Ω : Type u_1}
{E : Type u_2}
{ι : Type u_3}
[Preorder ι]
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{f : ι → Ω → E}
{ℱ : MeasureTheory.Filtration ι m0}
[Preorder E]
(hf : MeasureTheory.Martingale f ℱ μ)
:
theorem
MeasureTheory.Martingale.submartingale
{Ω : Type u_1}
{E : Type u_2}
{ι : Type u_3}
[Preorder ι]
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{f : ι → Ω → E}
{ℱ : MeasureTheory.Filtration ι m0}
[Preorder E]
(hf : MeasureTheory.Martingale f ℱ μ)
:
theorem
MeasureTheory.martingale_iff
{Ω : Type u_1}
{E : Type u_2}
{ι : Type u_3}
[Preorder ι]
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{f : ι → Ω → E}
{ℱ : MeasureTheory.Filtration ι m0}
[PartialOrder E]
:
MeasureTheory.Martingale f ℱ μ ↔ MeasureTheory.Supermartingale f ℱ μ ∧ MeasureTheory.Submartingale f ℱ μ
theorem
MeasureTheory.martingale_condexp
{Ω : Type u_1}
{E : Type u_2}
{ι : Type u_3}
[Preorder ι]
{m0 : MeasurableSpace Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
(f : Ω → E)
(ℱ : MeasureTheory.Filtration ι m0)
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.SigmaFiniteFiltration μ ℱ]
:
MeasureTheory.Martingale (fun (i : ι) => MeasureTheory.condexp (↑ℱ i) μ f) ℱ μ
theorem
MeasureTheory.Supermartingale.adapted
{Ω : Type u_1}
{E : Type u_2}
{ι : Type u_3}
[Preorder ι]
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{f : ι → Ω → E}
{ℱ : MeasureTheory.Filtration ι m0}
[LE E]
(hf : MeasureTheory.Supermartingale f ℱ μ)
:
theorem
MeasureTheory.Supermartingale.stronglyMeasurable
{Ω : Type u_1}
{E : Type u_2}
{ι : Type u_3}
[Preorder ι]
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{f : ι → Ω → E}
{ℱ : MeasureTheory.Filtration ι m0}
[LE E]
(hf : MeasureTheory.Supermartingale f ℱ μ)
(i : ι)
:
theorem
MeasureTheory.Supermartingale.integrable
{Ω : Type u_1}
{E : Type u_2}
{ι : Type u_3}
[Preorder ι]
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{f : ι → Ω → E}
{ℱ : MeasureTheory.Filtration ι m0}
[LE E]
(hf : MeasureTheory.Supermartingale f ℱ μ)
(i : ι)
:
MeasureTheory.Integrable (f i)
theorem
MeasureTheory.Supermartingale.condexp_ae_le
{Ω : Type u_1}
{E : Type u_2}
{ι : Type u_3}
[Preorder ι]
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{f : ι → Ω → E}
{ℱ : MeasureTheory.Filtration ι m0}
[LE E]
(hf : MeasureTheory.Supermartingale f ℱ μ)
{i : ι}
{j : ι}
(hij : i ≤ j)
:
MeasureTheory.condexp (↑ℱ i) μ (f j) ≤ᶠ[MeasureTheory.Measure.ae μ] f i
theorem
MeasureTheory.Supermartingale.set_integral_le
{Ω : Type u_1}
{ι : Type u_3}
[Preorder ι]
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{ℱ : MeasureTheory.Filtration ι m0}
[MeasureTheory.SigmaFiniteFiltration μ ℱ]
{f : ι → Ω → ℝ}
(hf : MeasureTheory.Supermartingale f ℱ μ)
{i : ι}
{j : ι}
(hij : i ≤ j)
{s : Set Ω}
(hs : MeasurableSet s)
:
∫ (ω : Ω) in s, f j ω ∂μ ≤ ∫ (ω : Ω) in s, f i ω ∂μ
theorem
MeasureTheory.Supermartingale.add
{Ω : Type u_1}
{E : Type u_2}
{ι : Type u_3}
[Preorder ι]
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{f : ι → Ω → E}
{g : ι → Ω → E}
{ℱ : MeasureTheory.Filtration ι m0}
[Preorder E]
[CovariantClass E E (fun (x x_1 : E) => x + x_1) fun (x x_1 : E) => x ≤ x_1]
(hf : MeasureTheory.Supermartingale f ℱ μ)
(hg : MeasureTheory.Supermartingale g ℱ μ)
:
MeasureTheory.Supermartingale (f + g) ℱ μ
theorem
MeasureTheory.Supermartingale.add_martingale
{Ω : Type u_1}
{E : Type u_2}
{ι : Type u_3}
[Preorder ι]
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{f : ι → Ω → E}
{g : ι → Ω → E}
{ℱ : MeasureTheory.Filtration ι m0}
[Preorder E]
[CovariantClass E E (fun (x x_1 : E) => x + x_1) fun (x x_1 : E) => x ≤ x_1]
(hf : MeasureTheory.Supermartingale f ℱ μ)
(hg : MeasureTheory.Martingale g ℱ μ)
:
MeasureTheory.Supermartingale (f + g) ℱ μ
theorem
MeasureTheory.Supermartingale.neg
{Ω : Type u_1}
{E : Type u_2}
{ι : Type u_3}
[Preorder ι]
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{f : ι → Ω → E}
{ℱ : MeasureTheory.Filtration ι m0}
[Preorder E]
[CovariantClass E E (fun (x x_1 : E) => x + x_1) fun (x x_1 : E) => x ≤ x_1]
(hf : MeasureTheory.Supermartingale f ℱ μ)
:
MeasureTheory.Submartingale (-f) ℱ μ
theorem
MeasureTheory.Submartingale.adapted
{Ω : Type u_1}
{E : Type u_2}
{ι : Type u_3}
[Preorder ι]
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{f : ι → Ω → E}
{ℱ : MeasureTheory.Filtration ι m0}
[LE E]
(hf : MeasureTheory.Submartingale f ℱ μ)
:
theorem
MeasureTheory.Submartingale.stronglyMeasurable
{Ω : Type u_1}
{E : Type u_2}
{ι : Type u_3}
[Preorder ι]
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{f : ι → Ω → E}
{ℱ : MeasureTheory.Filtration ι m0}
[LE E]
(hf : MeasureTheory.Submartingale f ℱ μ)
(i : ι)
:
theorem
MeasureTheory.Submartingale.integrable
{Ω : Type u_1}
{E : Type u_2}
{ι : Type u_3}
[Preorder ι]
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{f : ι → Ω → E}
{ℱ : MeasureTheory.Filtration ι m0}
[LE E]
(hf : MeasureTheory.Submartingale f ℱ μ)
(i : ι)
:
MeasureTheory.Integrable (f i)
theorem
MeasureTheory.Submartingale.ae_le_condexp
{Ω : Type u_1}
{E : Type u_2}
{ι : Type u_3}
[Preorder ι]
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{f : ι → Ω → E}
{ℱ : MeasureTheory.Filtration ι m0}
[LE E]
(hf : MeasureTheory.Submartingale f ℱ μ)
{i : ι}
{j : ι}
(hij : i ≤ j)
:
f i ≤ᶠ[MeasureTheory.Measure.ae μ] MeasureTheory.condexp (↑ℱ i) μ (f j)
theorem
MeasureTheory.Submartingale.add
{Ω : Type u_1}
{E : Type u_2}
{ι : Type u_3}
[Preorder ι]
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{f : ι → Ω → E}
{g : ι → Ω → E}
{ℱ : MeasureTheory.Filtration ι m0}
[Preorder E]
[CovariantClass E E (fun (x x_1 : E) => x + x_1) fun (x x_1 : E) => x ≤ x_1]
(hf : MeasureTheory.Submartingale f ℱ μ)
(hg : MeasureTheory.Submartingale g ℱ μ)
:
MeasureTheory.Submartingale (f + g) ℱ μ
theorem
MeasureTheory.Submartingale.add_martingale
{Ω : Type u_1}
{E : Type u_2}
{ι : Type u_3}
[Preorder ι]
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{f : ι → Ω → E}
{g : ι → Ω → E}
{ℱ : MeasureTheory.Filtration ι m0}
[Preorder E]
[CovariantClass E E (fun (x x_1 : E) => x + x_1) fun (x x_1 : E) => x ≤ x_1]
(hf : MeasureTheory.Submartingale f ℱ μ)
(hg : MeasureTheory.Martingale g ℱ μ)
:
MeasureTheory.Submartingale (f + g) ℱ μ
theorem
MeasureTheory.Submartingale.neg
{Ω : Type u_1}
{E : Type u_2}
{ι : Type u_3}
[Preorder ι]
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{f : ι → Ω → E}
{ℱ : MeasureTheory.Filtration ι m0}
[Preorder E]
[CovariantClass E E (fun (x x_1 : E) => x + x_1) fun (x x_1 : E) => x ≤ x_1]
(hf : MeasureTheory.Submartingale f ℱ μ)
:
MeasureTheory.Supermartingale (-f) ℱ μ
theorem
MeasureTheory.Submartingale.set_integral_le
{Ω : Type u_1}
{ι : Type u_3}
[Preorder ι]
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{ℱ : MeasureTheory.Filtration ι m0}
[MeasureTheory.SigmaFiniteFiltration μ ℱ]
{f : ι → Ω → ℝ}
(hf : MeasureTheory.Submartingale f ℱ μ)
{i : ι}
{j : ι}
(hij : i ≤ j)
{s : Set Ω}
(hs : MeasurableSet s)
:
∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f j ω ∂μ
The converse of this lemma is MeasureTheory.submartingale_of_set_integral_le.
theorem
MeasureTheory.Submartingale.sub_supermartingale
{Ω : Type u_1}
{E : Type u_2}
{ι : Type u_3}
[Preorder ι]
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{f : ι → Ω → E}
{g : ι → Ω → E}
{ℱ : MeasureTheory.Filtration ι m0}
[Preorder E]
[CovariantClass E E (fun (x x_1 : E) => x + x_1) fun (x x_1 : E) => x ≤ x_1]
(hf : MeasureTheory.Submartingale f ℱ μ)
(hg : MeasureTheory.Supermartingale g ℱ μ)
:
MeasureTheory.Submartingale (f - g) ℱ μ
theorem
MeasureTheory.Submartingale.sub_martingale
{Ω : Type u_1}
{E : Type u_2}
{ι : Type u_3}
[Preorder ι]
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{f : ι → Ω → E}
{g : ι → Ω → E}
{ℱ : MeasureTheory.Filtration ι m0}
[Preorder E]
[CovariantClass E E (fun (x x_1 : E) => x + x_1) fun (x x_1 : E) => x ≤ x_1]
(hf : MeasureTheory.Submartingale f ℱ μ)
(hg : MeasureTheory.Martingale g ℱ μ)
:
MeasureTheory.Submartingale (f - g) ℱ μ
theorem
MeasureTheory.Submartingale.sup
{Ω : Type u_1}
{ι : Type u_3}
[Preorder ι]
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{ℱ : MeasureTheory.Filtration ι m0}
{f : ι → Ω → ℝ}
{g : ι → Ω → ℝ}
(hf : MeasureTheory.Submartingale f ℱ μ)
(hg : MeasureTheory.Submartingale g ℱ μ)
:
MeasureTheory.Submartingale (f ⊔ g) ℱ μ
theorem
MeasureTheory.Submartingale.pos
{Ω : Type u_1}
{ι : Type u_3}
[Preorder ι]
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{ℱ : MeasureTheory.Filtration ι m0}
{f : ι → Ω → ℝ}
(hf : MeasureTheory.Submartingale f ℱ μ)
:
theorem
MeasureTheory.submartingale_of_set_integral_le
{Ω : Type u_1}
{ι : Type u_3}
[Preorder ι]
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{ℱ : MeasureTheory.Filtration ι m0}
[MeasureTheory.IsFiniteMeasure μ]
{f : ι → Ω → ℝ}
(hadp : MeasureTheory.Adapted ℱ f)
(hint : ∀ (i : ι), MeasureTheory.Integrable (f i))
(hf : ∀ (i j : ι), i ≤ j → ∀ (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f j ω ∂μ)
:
theorem
MeasureTheory.submartingale_of_condexp_sub_nonneg
{Ω : Type u_1}
{ι : Type u_3}
[Preorder ι]
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{ℱ : MeasureTheory.Filtration ι m0}
[MeasureTheory.IsFiniteMeasure μ]
{f : ι → Ω → ℝ}
(hadp : MeasureTheory.Adapted ℱ f)
(hint : ∀ (i : ι), MeasureTheory.Integrable (f i))
(hf : ∀ (i j : ι), i ≤ j → 0 ≤ᶠ[MeasureTheory.Measure.ae μ] MeasureTheory.condexp (↑ℱ i) μ (f j - f i))
:
theorem
MeasureTheory.Submartingale.condexp_sub_nonneg
{Ω : Type u_1}
{ι : Type u_3}
[Preorder ι]
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{ℱ : MeasureTheory.Filtration ι m0}
{f : ι → Ω → ℝ}
(hf : MeasureTheory.Submartingale f ℱ μ)
{i : ι}
{j : ι}
(hij : i ≤ j)
:
0 ≤ᶠ[MeasureTheory.Measure.ae μ] MeasureTheory.condexp (↑ℱ i) μ (f j - f i)
theorem
MeasureTheory.submartingale_iff_condexp_sub_nonneg
{Ω : Type u_1}
{ι : Type u_3}
[Preorder ι]
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{ℱ : MeasureTheory.Filtration ι m0}
[MeasureTheory.IsFiniteMeasure μ]
{f : ι → Ω → ℝ}
:
MeasureTheory.Submartingale f ℱ μ ↔ MeasureTheory.Adapted ℱ f ∧ (∀ (i : ι), MeasureTheory.Integrable (f i)) ∧ ∀ (i j : ι), i ≤ j → 0 ≤ᶠ[MeasureTheory.Measure.ae μ] MeasureTheory.condexp (↑ℱ i) μ (f j - f i)
theorem
MeasureTheory.Supermartingale.sub_submartingale
{Ω : Type u_1}
{E : Type u_2}
{ι : Type u_3}
[Preorder ι]
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{f : ι → Ω → E}
{g : ι → Ω → E}
{ℱ : MeasureTheory.Filtration ι m0}
[Preorder E]
[CovariantClass E E (fun (x x_1 : E) => x + x_1) fun (x x_1 : E) => x ≤ x_1]
(hf : MeasureTheory.Supermartingale f ℱ μ)
(hg : MeasureTheory.Submartingale g ℱ μ)
:
MeasureTheory.Supermartingale (f - g) ℱ μ
theorem
MeasureTheory.Supermartingale.sub_martingale
{Ω : Type u_1}
{E : Type u_2}
{ι : Type u_3}
[Preorder ι]
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{f : ι → Ω → E}
{g : ι → Ω → E}
{ℱ : MeasureTheory.Filtration ι m0}
[Preorder E]
[CovariantClass E E (fun (x x_1 : E) => x + x_1) fun (x x_1 : E) => x ≤ x_1]
(hf : MeasureTheory.Supermartingale f ℱ μ)
(hg : MeasureTheory.Martingale g ℱ μ)
:
MeasureTheory.Supermartingale (f - g) ℱ μ
theorem
MeasureTheory.Supermartingale.smul_nonneg
{Ω : Type u_1}
{ι : Type u_3}
[Preorder ι]
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{ℱ : MeasureTheory.Filtration ι m0}
{F : Type u_4}
[NormedLatticeAddCommGroup F]
[NormedSpace ℝ F]
[CompleteSpace F]
[OrderedSMul ℝ F]
{f : ι → Ω → F}
{c : ℝ}
(hc : 0 ≤ c)
(hf : MeasureTheory.Supermartingale f ℱ μ)
:
MeasureTheory.Supermartingale (c • f) ℱ μ
theorem
MeasureTheory.Supermartingale.smul_nonpos
{Ω : Type u_1}
{ι : Type u_3}
[Preorder ι]
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{ℱ : MeasureTheory.Filtration ι m0}
{F : Type u_4}
[NormedLatticeAddCommGroup F]
[NormedSpace ℝ F]
[CompleteSpace F]
[OrderedSMul ℝ F]
{f : ι → Ω → F}
{c : ℝ}
(hc : c ≤ 0)
(hf : MeasureTheory.Supermartingale f ℱ μ)
:
MeasureTheory.Submartingale (c • f) ℱ μ
theorem
MeasureTheory.Submartingale.smul_nonneg
{Ω : Type u_1}
{ι : Type u_3}
[Preorder ι]
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{ℱ : MeasureTheory.Filtration ι m0}
{F : Type u_4}
[NormedLatticeAddCommGroup F]
[NormedSpace ℝ F]
[CompleteSpace F]
[OrderedSMul ℝ F]
{f : ι → Ω → F}
{c : ℝ}
(hc : 0 ≤ c)
(hf : MeasureTheory.Submartingale f ℱ μ)
:
MeasureTheory.Submartingale (c • f) ℱ μ
theorem
MeasureTheory.Submartingale.smul_nonpos
{Ω : Type u_1}
{ι : Type u_3}
[Preorder ι]
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{ℱ : MeasureTheory.Filtration ι m0}
{F : Type u_4}
[NormedLatticeAddCommGroup F]
[NormedSpace ℝ F]
[CompleteSpace F]
[OrderedSMul ℝ F]
{f : ι → Ω → F}
{c : ℝ}
(hc : c ≤ 0)
(hf : MeasureTheory.Submartingale f ℱ μ)
:
MeasureTheory.Supermartingale (c • f) ℱ μ
theorem
MeasureTheory.submartingale_of_set_integral_le_succ
{Ω : Type u_1}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{𝒢 : MeasureTheory.Filtration ℕ m0}
[MeasureTheory.IsFiniteMeasure μ]
{f : ℕ → Ω → ℝ}
(hadp : MeasureTheory.Adapted 𝒢 f)
(hint : ∀ (i : ℕ), MeasureTheory.Integrable (f i))
(hf : ∀ (i : ℕ) (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f (i + 1) ω ∂μ)
:
theorem
MeasureTheory.supermartingale_of_set_integral_succ_le
{Ω : Type u_1}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{𝒢 : MeasureTheory.Filtration ℕ m0}
[MeasureTheory.IsFiniteMeasure μ]
{f : ℕ → Ω → ℝ}
(hadp : MeasureTheory.Adapted 𝒢 f)
(hint : ∀ (i : ℕ), MeasureTheory.Integrable (f i))
(hf : ∀ (i : ℕ) (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, f (i + 1) ω ∂μ ≤ ∫ (ω : Ω) in s, f i ω ∂μ)
:
theorem
MeasureTheory.martingale_of_set_integral_eq_succ
{Ω : Type u_1}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{𝒢 : MeasureTheory.Filtration ℕ m0}
[MeasureTheory.IsFiniteMeasure μ]
{f : ℕ → Ω → ℝ}
(hadp : MeasureTheory.Adapted 𝒢 f)
(hint : ∀ (i : ℕ), MeasureTheory.Integrable (f i))
(hf : ∀ (i : ℕ) (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, f i ω ∂μ = ∫ (ω : Ω) in s, f (i + 1) ω ∂μ)
:
MeasureTheory.Martingale f 𝒢 μ
theorem
MeasureTheory.submartingale_nat
{Ω : Type u_1}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{𝒢 : MeasureTheory.Filtration ℕ m0}
[MeasureTheory.IsFiniteMeasure μ]
{f : ℕ → Ω → ℝ}
(hadp : MeasureTheory.Adapted 𝒢 f)
(hint : ∀ (i : ℕ), MeasureTheory.Integrable (f i))
(hf : ∀ (i : ℕ), f i ≤ᶠ[MeasureTheory.Measure.ae μ] MeasureTheory.condexp (↑𝒢 i) μ (f (i + 1)))
:
theorem
MeasureTheory.supermartingale_nat
{Ω : Type u_1}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{𝒢 : MeasureTheory.Filtration ℕ m0}
[MeasureTheory.IsFiniteMeasure μ]
{f : ℕ → Ω → ℝ}
(hadp : MeasureTheory.Adapted 𝒢 f)
(hint : ∀ (i : ℕ), MeasureTheory.Integrable (f i))
(hf : ∀ (i : ℕ), MeasureTheory.condexp (↑𝒢 i) μ (f (i + 1)) ≤ᶠ[MeasureTheory.Measure.ae μ] f i)
:
theorem
MeasureTheory.martingale_nat
{Ω : Type u_1}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{𝒢 : MeasureTheory.Filtration ℕ m0}
[MeasureTheory.IsFiniteMeasure μ]
{f : ℕ → Ω → ℝ}
(hadp : MeasureTheory.Adapted 𝒢 f)
(hint : ∀ (i : ℕ), MeasureTheory.Integrable (f i))
(hf : ∀ (i : ℕ), f i =ᶠ[MeasureTheory.Measure.ae μ] MeasureTheory.condexp (↑𝒢 i) μ (f (i + 1)))
:
MeasureTheory.Martingale f 𝒢 μ
theorem
MeasureTheory.submartingale_of_condexp_sub_nonneg_nat
{Ω : Type u_1}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{𝒢 : MeasureTheory.Filtration ℕ m0}
[MeasureTheory.IsFiniteMeasure μ]
{f : ℕ → Ω → ℝ}
(hadp : MeasureTheory.Adapted 𝒢 f)
(hint : ∀ (i : ℕ), MeasureTheory.Integrable (f i))
(hf : ∀ (i : ℕ), 0 ≤ᶠ[MeasureTheory.Measure.ae μ] MeasureTheory.condexp (↑𝒢 i) μ (f (i + 1) - f i))
:
theorem
MeasureTheory.supermartingale_of_condexp_sub_nonneg_nat
{Ω : Type u_1}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{𝒢 : MeasureTheory.Filtration ℕ m0}
[MeasureTheory.IsFiniteMeasure μ]
{f : ℕ → Ω → ℝ}
(hadp : MeasureTheory.Adapted 𝒢 f)
(hint : ∀ (i : ℕ), MeasureTheory.Integrable (f i))
(hf : ∀ (i : ℕ), 0 ≤ᶠ[MeasureTheory.Measure.ae μ] MeasureTheory.condexp (↑𝒢 i) μ (f i - f (i + 1)))
:
theorem
MeasureTheory.martingale_of_condexp_sub_eq_zero_nat
{Ω : Type u_1}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{𝒢 : MeasureTheory.Filtration ℕ m0}
[MeasureTheory.IsFiniteMeasure μ]
{f : ℕ → Ω → ℝ}
(hadp : MeasureTheory.Adapted 𝒢 f)
(hint : ∀ (i : ℕ), MeasureTheory.Integrable (f i))
(hf : ∀ (i : ℕ), MeasureTheory.condexp (↑𝒢 i) μ (f (i + 1) - f i) =ᶠ[MeasureTheory.Measure.ae μ] 0)
:
MeasureTheory.Martingale f 𝒢 μ
theorem
MeasureTheory.Submartingale.zero_le_of_predictable
{Ω : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{𝒢 : MeasureTheory.Filtration ℕ m0}
[Preorder E]
[MeasureTheory.SigmaFiniteFiltration μ 𝒢]
{f : ℕ → Ω → E}
(hfmgle : MeasureTheory.Submartingale f 𝒢 μ)
(hfadp : MeasureTheory.Adapted 𝒢 fun (n : ℕ) => f (n + 1))
(n : ℕ)
:
f 0 ≤ᶠ[MeasureTheory.Measure.ae μ] f n
A predictable submartingale is a.e. greater equal than its initial state.
theorem
MeasureTheory.Supermartingale.le_zero_of_predictable
{Ω : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{𝒢 : MeasureTheory.Filtration ℕ m0}
[Preorder E]
[MeasureTheory.SigmaFiniteFiltration μ 𝒢]
{f : ℕ → Ω → E}
(hfmgle : MeasureTheory.Supermartingale f 𝒢 μ)
(hfadp : MeasureTheory.Adapted 𝒢 fun (n : ℕ) => f (n + 1))
(n : ℕ)
:
f n ≤ᶠ[MeasureTheory.Measure.ae μ] f 0
A predictable supermartingale is a.e. less equal than its initial state.
theorem
MeasureTheory.Martingale.eq_zero_of_predictable
{Ω : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{𝒢 : MeasureTheory.Filtration ℕ m0}
[MeasureTheory.SigmaFiniteFiltration μ 𝒢]
{f : ℕ → Ω → E}
(hfmgle : MeasureTheory.Martingale f 𝒢 μ)
(hfadp : MeasureTheory.Adapted 𝒢 fun (n : ℕ) => f (n + 1))
(n : ℕ)
:
f n =ᶠ[MeasureTheory.Measure.ae μ] f 0
A predictable martingale is a.e. equal to its initial state.
theorem
MeasureTheory.Submartingale.integrable_stoppedValue
{Ω : Type u_1}
{E : Type u_2}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{𝒢 : MeasureTheory.Filtration ℕ m0}
[LE E]
{f : ℕ → Ω → E}
(hf : MeasureTheory.Submartingale f 𝒢 μ)
{τ : Ω → ℕ}
(hτ : MeasureTheory.IsStoppingTime 𝒢 τ)
{N : ℕ}
(hbdd : ∀ (ω : Ω), τ ω ≤ N)
:
theorem
MeasureTheory.Submartingale.sum_mul_sub
{Ω : Type u_1}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{𝒢 : MeasureTheory.Filtration ℕ m0}
[MeasureTheory.IsFiniteMeasure μ]
{R : ℝ}
{ξ : ℕ → Ω → ℝ}
{f : ℕ → Ω → ℝ}
(hf : MeasureTheory.Submartingale f 𝒢 μ)
(hξ : MeasureTheory.Adapted 𝒢 ξ)
(hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R)
(hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω)
:
MeasureTheory.Submartingale (fun (n : ℕ) => Finset.sum (Finset.range n) fun (k : ℕ) => ξ k * (f (k + 1) - f k)) 𝒢 μ
theorem
MeasureTheory.Submartingale.sum_mul_sub'
{Ω : Type u_1}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{𝒢 : MeasureTheory.Filtration ℕ m0}
[MeasureTheory.IsFiniteMeasure μ]
{R : ℝ}
{ξ : ℕ → Ω → ℝ}
{f : ℕ → Ω → ℝ}
(hf : MeasureTheory.Submartingale f 𝒢 μ)
(hξ : MeasureTheory.Adapted 𝒢 fun (n : ℕ) => ξ (n + 1))
(hbdd : ∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R)
(hnonneg : ∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω)
:
MeasureTheory.Submartingale (fun (n : ℕ) => Finset.sum (Finset.range n) fun (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 fun n => ∑ k in Finset.range n, ξ (k + 1) * (f (k + 1) - f k) is also a
submartingale.