Optional sampling theorem #
If τ is a bounded stopping time and σ is another stopping time, then the value of a martingale
f at the stopping time min τ σ is almost everywhere equal to
μ[stoppedValue f τ | hσ.measurableSpace].
Main results #
stoppedValue_ae_eq_condexp_of_le_const: the value of a martingalefat a stopping timeτbounded bynis the conditional expectation off nwith respect to the σ-algebra generated byτ.stoppedValue_ae_eq_condexp_of_le: ifτandσare two stopping times withσ ≤ τandτis bounded, then the value of a martingalefatσis the conditional expectation of its value atτwith respect to the σ-algebra generated byσ.stoppedValue_min_ae_eq_condexp: the optional sampling theorem. Ifτis a bounded stopping time andσis another stopping time, then the value of a martingalefat the stopping timemin τ σis almost everywhere equal to the conditional expectation offstopped atτwith respect to the σ-algebra generated byσ.
instance
DiscreteTopology.secondCountableTopology_of_countable
{α : Type u_1}
[TopologicalSpace α]
[DiscreteTopology α]
[Countable α]
:
Equations
- (_ : SecondCountableTopology α) = (_ : SecondCountableTopology α)
theorem
MeasureTheory.Martingale.condexp_stopping_time_ae_eq_restrict_eq_const
{Ω : Type u_1}
{E : Type u_2}
{m : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{ι : Type u_3}
[LinearOrder ι]
[TopologicalSpace ι]
[OrderTopology ι]
[FirstCountableTopology ι]
{ℱ : MeasureTheory.Filtration ι m}
[MeasureTheory.SigmaFiniteFiltration μ ℱ]
{τ : Ω → ι}
{f : ι → Ω → E}
{i : ι}
{n : ι}
[Filter.IsCountablyGenerated Filter.atTop]
(h : MeasureTheory.Martingale f ℱ μ)
(hτ : MeasureTheory.IsStoppingTime ℱ τ)
[MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ (_ : MeasureTheory.IsStoppingTime.measurableSpace hτ ≤ m))]
(hin : i ≤ n)
:
MeasureTheory.condexp (MeasureTheory.IsStoppingTime.measurableSpace hτ) μ
(f n) =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ {x : Ω | τ x = i})] f i
theorem
MeasureTheory.Martingale.condexp_stopping_time_ae_eq_restrict_eq_const_of_le_const
{Ω : Type u_1}
{E : Type u_2}
{m : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{ι : Type u_3}
[LinearOrder ι]
[TopologicalSpace ι]
[OrderTopology ι]
[FirstCountableTopology ι]
{ℱ : MeasureTheory.Filtration ι m}
[MeasureTheory.SigmaFiniteFiltration μ ℱ]
{τ : Ω → ι}
{f : ι → Ω → E}
{n : ι}
(h : MeasureTheory.Martingale f ℱ μ)
(hτ : MeasureTheory.IsStoppingTime ℱ τ)
(hτ_le : ∀ (x : Ω), τ x ≤ n)
[MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ (_ : MeasureTheory.IsStoppingTime.measurableSpace hτ ≤ m))]
(i : ι)
:
MeasureTheory.condexp (MeasureTheory.IsStoppingTime.measurableSpace hτ) μ
(f n) =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ {x : Ω | τ x = i})] f i
theorem
MeasureTheory.Martingale.stoppedValue_ae_eq_restrict_eq
{Ω : Type u_1}
{E : Type u_2}
{m : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{ι : Type u_3}
[LinearOrder ι]
[TopologicalSpace ι]
[OrderTopology ι]
[FirstCountableTopology ι]
{ℱ : MeasureTheory.Filtration ι m}
[MeasureTheory.SigmaFiniteFiltration μ ℱ]
{τ : Ω → ι}
{f : ι → Ω → E}
{n : ι}
(h : MeasureTheory.Martingale f ℱ μ)
(hτ : MeasureTheory.IsStoppingTime ℱ τ)
(hτ_le : ∀ (x : Ω), τ x ≤ n)
[MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ (_ : MeasureTheory.IsStoppingTime.measurableSpace hτ ≤ m))]
(i : ι)
:
MeasureTheory.stoppedValue f τ =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ {x : Ω | τ x = i})] MeasureTheory.condexp (MeasureTheory.IsStoppingTime.measurableSpace hτ) μ (f n)
theorem
MeasureTheory.Martingale.stoppedValue_ae_eq_condexp_of_le_const_of_countable_range
{Ω : Type u_1}
{E : Type u_2}
{m : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{ι : Type u_3}
[LinearOrder ι]
[TopologicalSpace ι]
[OrderTopology ι]
[FirstCountableTopology ι]
{ℱ : MeasureTheory.Filtration ι m}
[MeasureTheory.SigmaFiniteFiltration μ ℱ]
{τ : Ω → ι}
{f : ι → Ω → E}
{n : ι}
(h : MeasureTheory.Martingale f ℱ μ)
(hτ : MeasureTheory.IsStoppingTime ℱ τ)
(hτ_le : ∀ (x : Ω), τ x ≤ n)
(h_countable_range : Set.Countable (Set.range τ))
[MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ (_ : MeasureTheory.IsStoppingTime.measurableSpace hτ ≤ m))]
:
The value of a martingale f at a stopping time τ bounded by n is the conditional
expectation of f n with respect to the σ-algebra generated by τ.
theorem
MeasureTheory.Martingale.stoppedValue_ae_eq_condexp_of_le_const
{Ω : Type u_1}
{E : Type u_2}
{m : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{ι : Type u_3}
[LinearOrder ι]
[TopologicalSpace ι]
[OrderTopology ι]
[FirstCountableTopology ι]
{ℱ : MeasureTheory.Filtration ι m}
[MeasureTheory.SigmaFiniteFiltration μ ℱ]
{τ : Ω → ι}
{f : ι → Ω → E}
{n : ι}
[Countable ι]
(h : MeasureTheory.Martingale f ℱ μ)
(hτ : MeasureTheory.IsStoppingTime ℱ τ)
(hτ_le : ∀ (x : Ω), τ x ≤ n)
[MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ (_ : MeasureTheory.IsStoppingTime.measurableSpace hτ ≤ m))]
:
The value of a martingale f at a stopping time τ bounded by n is the conditional
expectation of f n with respect to the σ-algebra generated by τ.
theorem
MeasureTheory.Martingale.stoppedValue_ae_eq_condexp_of_le_of_countable_range
{Ω : Type u_1}
{E : Type u_2}
{m : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{ι : Type u_3}
[LinearOrder ι]
[TopologicalSpace ι]
[OrderTopology ι]
[FirstCountableTopology ι]
{ℱ : MeasureTheory.Filtration ι m}
[MeasureTheory.SigmaFiniteFiltration μ ℱ]
{τ : Ω → ι}
{σ : Ω → ι}
{f : ι → Ω → E}
{n : ι}
(h : MeasureTheory.Martingale f ℱ μ)
(hτ : MeasureTheory.IsStoppingTime ℱ τ)
(hσ : MeasureTheory.IsStoppingTime ℱ σ)
(hσ_le_τ : σ ≤ τ)
(hτ_le : ∀ (x : Ω), τ x ≤ n)
(hτ_countable_range : Set.Countable (Set.range τ))
(hσ_countable_range : Set.Countable (Set.range σ))
[MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ (_ : MeasureTheory.IsStoppingTime.measurableSpace hσ ≤ m))]
:
If τ and σ are two stopping times with σ ≤ τ and τ is bounded, then the value of a
martingale f at σ is the conditional expectation of its value at τ with respect to the
σ-algebra generated by σ.
theorem
MeasureTheory.Martingale.stoppedValue_ae_eq_condexp_of_le
{Ω : Type u_1}
{E : Type u_2}
{m : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{ι : Type u_3}
[LinearOrder ι]
[TopologicalSpace ι]
[OrderTopology ι]
[FirstCountableTopology ι]
{ℱ : MeasureTheory.Filtration ι m}
[MeasureTheory.SigmaFiniteFiltration μ ℱ]
{τ : Ω → ι}
{σ : Ω → ι}
{f : ι → Ω → E}
{n : ι}
[Countable ι]
(h : MeasureTheory.Martingale f ℱ μ)
(hτ : MeasureTheory.IsStoppingTime ℱ τ)
(hσ : MeasureTheory.IsStoppingTime ℱ σ)
(hσ_le_τ : σ ≤ τ)
(hτ_le : ∀ (x : Ω), τ x ≤ n)
[MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ (_ : MeasureTheory.IsStoppingTime.measurableSpace hσ ≤ m))]
:
If τ and σ are two stopping times with σ ≤ τ and τ is bounded, then the value of a
martingale f at σ is the conditional expectation of its value at τ with respect to the
σ-algebra generated by σ.
In the following results the index set verifies
[LinearOrder ι] [LocallyFiniteOrder ι] [OrderBot ι], which means that it is order-isomorphic to
a subset of ℕ. ι is equipped with the discrete topology, which is also the order topology,
and is a measurable space with the Borel σ-algebra.
theorem
MeasureTheory.Martingale.condexp_stoppedValue_stopping_time_ae_eq_restrict_le
{Ω : Type u_1}
{E : Type u_2}
{m : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{ι : Type u_3}
[LinearOrder ι]
[LocallyFiniteOrder ι]
[OrderBot ι]
[TopologicalSpace ι]
[DiscreteTopology ι]
[MeasurableSpace ι]
[BorelSpace ι]
[MeasurableSpace E]
[BorelSpace E]
[SecondCountableTopology E]
{ℱ : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
{σ : Ω → ι}
{f : ι → Ω → E}
{n : ι}
(h : MeasureTheory.Martingale f ℱ μ)
(hτ : MeasureTheory.IsStoppingTime ℱ τ)
(hσ : MeasureTheory.IsStoppingTime ℱ σ)
[MeasureTheory.SigmaFinite (MeasureTheory.Measure.trim μ (_ : MeasureTheory.IsStoppingTime.measurableSpace hσ ≤ m))]
(hτ_le : ∀ (x : Ω), τ x ≤ n)
:
MeasureTheory.condexp (MeasureTheory.IsStoppingTime.measurableSpace hσ) μ
(MeasureTheory.stoppedValue f τ) =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.restrict μ {x : Ω | τ x ≤ σ x})] MeasureTheory.stoppedValue f τ
theorem
MeasureTheory.Martingale.stoppedValue_min_ae_eq_condexp
{Ω : Type u_1}
{E : Type u_2}
{m : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[CompleteSpace E]
{ι : Type u_3}
[LinearOrder ι]
[LocallyFiniteOrder ι]
[OrderBot ι]
[TopologicalSpace ι]
[DiscreteTopology ι]
[MeasurableSpace ι]
[BorelSpace ι]
[MeasurableSpace E]
[BorelSpace E]
[SecondCountableTopology E]
{ℱ : MeasureTheory.Filtration ι m}
{τ : Ω → ι}
{σ : Ω → ι}
{f : ι → Ω → E}
[MeasureTheory.SigmaFiniteFiltration μ ℱ]
(h : MeasureTheory.Martingale f ℱ μ)
(hτ : MeasureTheory.IsStoppingTime ℱ τ)
(hσ : MeasureTheory.IsStoppingTime ℱ σ)
{n : ι}
(hτ_le : ∀ (x : Ω), τ x ≤ n)
[h_sf_min : MeasureTheory.SigmaFinite
(MeasureTheory.Measure.trim μ
(_ :
MeasureTheory.IsStoppingTime.measurableSpace (_ : MeasureTheory.IsStoppingTime ℱ fun (ω : Ω) => min (τ ω) (σ ω)) ≤ m))]
:
(MeasureTheory.stoppedValue f fun (x : Ω) => min (σ x) (τ x)) =ᶠ[MeasureTheory.Measure.ae μ] MeasureTheory.condexp (MeasureTheory.IsStoppingTime.measurableSpace hσ) μ (MeasureTheory.stoppedValue f τ)
Optional Sampling theorem. If τ is a bounded stopping time and σ is another stopping
time, then the value of a martingale f at the stopping time min τ σ is almost everywhere equal
to the conditional expectation of f stopped at τ with respect to the σ-algebra generated
by σ.