# 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 #

• stoppedValue_ae_eq_condexp_of_le_const: 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 τ.
• stoppedValue_ae_eq_condexp_of_le: 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 σ.
• 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 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 σ.
theorem MeasureTheory.Martingale.condexp_stopping_time_ae_eq_restrict_eq_const {Ω : Type u_1} {E : Type u_2} {m : } {μ : } [] [] {ι : Type u_3} [] [] [] {ℱ : } {τ : Ωι} {f : ιΩE} {i : ι} {n : ι} [Filter.IsCountablyGenerated Filter.atTop] (h : ) (hτ : ) (hin : i n) :
theorem MeasureTheory.Martingale.condexp_stopping_time_ae_eq_restrict_eq_const_of_le_const {Ω : Type u_1} {E : Type u_2} {m : } {μ : } [] [] {ι : Type u_3} [] [] [] {ℱ : } {τ : Ωι} {f : ιΩE} {n : ι} (h : ) (hτ : ) (hτ_le : ∀ (x : Ω), τ x n) (i : ι) :
theorem MeasureTheory.Martingale.stoppedValue_ae_eq_restrict_eq {Ω : Type u_1} {E : Type u_2} {m : } {μ : } [] [] {ι : Type u_3} [] [] [] {ℱ : } {τ : Ωι} {f : ιΩE} {n : ι} (h : ) (hτ : ) (hτ_le : ∀ (x : Ω), τ x n) (i : ι) :
theorem MeasureTheory.Martingale.stoppedValue_ae_eq_condexp_of_le_const_of_countable_range {Ω : Type u_1} {E : Type u_2} {m : } {μ : } [] [] {ι : Type u_3} [] [] [] {ℱ : } {τ : Ωι} {f : ιΩE} {n : ι} (h : ) (hτ : ) (hτ_le : ∀ (x : Ω), τ x n) (h_countable_range : ) :

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 : } {μ : } [] [] {ι : Type u_3} [] [] [] {ℱ : } {τ : Ωι} {f : ιΩE} {n : ι} [] (h : ) (hτ : ) (hτ_le : ∀ (x : Ω), τ x 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 : } {μ : } [] [] {ι : Type u_3} [] [] [] {ℱ : } {τ : Ωι} {σ : Ωι} {f : ιΩE} {n : ι} (h : ) (hτ : ) (hσ : ) (hσ_le_τ : σ τ) (hτ_le : ∀ (x : Ω), τ x n) (hτ_countable_range : ) (hσ_countable_range : ) :

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 : } {μ : } [] [] {ι : Type u_3} [] [] [] {ℱ : } {τ : Ωι} {σ : Ωι} {f : ιΩE} {n : ι} [] (h : ) (hτ : ) (hσ : ) (hσ_le_τ : σ τ) (hτ_le : ∀ (x : Ω), τ x n) :

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 : } {μ : } [] [] {ι : Type u_3} [] [] [] [] [] [] [] [] {ℱ : } {τ : Ωι} {σ : Ωι} {f : ιΩE} {n : ι} (h : ) (hτ : ) (hσ : ) (hτ_le : ∀ (x : Ω), τ x n) :
theorem MeasureTheory.Martingale.stoppedValue_min_ae_eq_condexp {Ω : Type u_1} {E : Type u_2} {m : } {μ : } [] [] {ι : Type u_3} [] [] [] [] [] [] [] [] {ℱ : } {τ : Ωι} {σ : Ωι} {f : ιΩE} (h : ) (hτ : ) (hσ : ) {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)) =ᶠ[]

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 σ.