Documentation

Mathlib.Probability.Martingale.OptionalSampling

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 #

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.atTop.IsCountablyGenerated] (h : MeasureTheory.Martingale f μ) (hτ : MeasureTheory.IsStoppingTime τ) [MeasureTheory.SigmaFinite (μ.trim )] (hin : i n) :
MeasureTheory.condexp .measurableSpace μ (f n) =ᵐ[μ.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 (μ.trim )] (i : ι) :
MeasureTheory.condexp .measurableSpace μ (f n) =ᵐ[μ.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 (μ.trim )] (i : ι) :
MeasureTheory.stoppedValue f τ =ᵐ[μ.restrict {x : Ω | τ x = i}] MeasureTheory.condexp .measurableSpace μ (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.range τ).Countable) [MeasureTheory.SigmaFinite (μ.trim )] :
MeasureTheory.stoppedValue f τ =ᵐ[μ] MeasureTheory.condexp .measurableSpace μ (f n)

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 (μ.trim )] :
MeasureTheory.stoppedValue f τ =ᵐ[μ] MeasureTheory.condexp .measurableSpace μ (f n)

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.range τ).Countable) (hσ_countable_range : (Set.range σ).Countable) [MeasureTheory.SigmaFinite (μ.trim )] :

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 (μ.trim )] :

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 (μ.trim )] (hτ_le : ∀ (x : Ω), τ x n) :
MeasureTheory.condexp .measurableSpace μ (MeasureTheory.stoppedValue f τ) =ᵐ[μ.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 (μ.trim )] :
(MeasureTheory.stoppedValue f fun (x : Ω) => min (σ x) (τ x)) =ᵐ[μ] MeasureTheory.condexp .measurableSpace μ (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 σ.