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

source
theorem MeasureTheory.Martingale.condExp_stopping_time_ae_eq_restrict_eq_const {Ω : Type u_1} {E : Type u_2} {m : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {ι : Type u_3} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι] {ℱ : Filtration ι m} [SigmaFiniteFiltration μ ℱ] {τ : Ω → WithTop ι} {f : ι → Ω → E} {i n : ι} (h : Martingale f ℱ μ) (hτ : IsStoppingTime ℱ τ) [SigmaFinite (μ.trim ⋯)] (hin : i ≤ n) :
μ[f n|hτ.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x = ↑i})] f i
source
theorem MeasureTheory.Martingale.condExp_stopping_time_ae_eq_restrict_eq_const_of_le_const {Ω : Type u_1} {E : Type u_2} {m : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {ι : Type u_3} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι] {ℱ : Filtration ι m} [SigmaFiniteFiltration μ ℱ] {τ : Ω → WithTop ι} {f : ι → Ω → E} {n : ι} (h : Martingale f ℱ μ) (hτ : IsStoppingTime ℱ τ) (hτ_le : ∀ (x : Ω), τ x ≤ ↑n) [SigmaFinite (μ.trim ⋯)] (i : ι) :
μ[f n|hτ.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x = ↑i})] f i
source
theorem MeasureTheory.Martingale.stoppedValue_ae_eq_restrict_eq {Ω : Type u_1} {E : Type u_2} {m : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {ι : Type u_3} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι] {ℱ : Filtration ι m} [SigmaFiniteFiltration μ ℱ] {τ : Ω → WithTop ι} {f : ι → Ω → E} {n : ι} [Nonempty ι] (h : Martingale f ℱ μ) (hτ : IsStoppingTime ℱ τ) (hτ_le : ∀ (x : Ω), τ x ≤ ↑n) [SigmaFinite (μ.trim ⋯)] (i : ι) :
stoppedValue f τ =ᶠ[ae (μ.restrict {x : Ω | τ x = ↑i})] μ[f n|hτ.measurableSpace]
source
theorem MeasureTheory.Martingale.stoppedValue_ae_eq_condExp_of_le_const_of_countable_range {Ω : Type u_1} {E : Type u_2} {m : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {ι : Type u_3} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι] {ℱ : Filtration ι m} [SigmaFiniteFiltration μ ℱ] {τ : Ω → WithTop ι} {f : ι → Ω → E} {n : ι} [Nonempty ι] (h : Martingale f ℱ μ) (hτ : IsStoppingTime ℱ τ) (hτ_le : ∀ (x : Ω), τ x ≤ ↑n) (h_countable_range : (Set.range τ).Countable) [SigmaFinite (μ.trim ⋯)] :
stoppedValue f τ =ᶠ[ae μ] μ[f n|hτ.measurableSpace]

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 `τ`.

source
theorem MeasureTheory.Martingale.stoppedValue_ae_eq_condExp_of_le_const {Ω : Type u_1} {E : Type u_2} {m : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {ι : Type u_3} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι] {ℱ : Filtration ι m} [SigmaFiniteFiltration μ ℱ] {τ : Ω → WithTop ι} {f : ι → Ω → E} {n : ι} [Nonempty ι] [Countable ι] (h : Martingale f ℱ μ) (hτ : IsStoppingTime ℱ τ) (hτ_le : ∀ (x : Ω), τ x ≤ ↑n) [SigmaFinite (μ.trim ⋯)] :
stoppedValue f τ =ᶠ[ae μ] μ[f n|hτ.measurableSpace]

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 `τ`.

source
theorem MeasureTheory.Martingale.stoppedValue_ae_eq_condExp_of_le_of_countable_range {Ω : Type u_1} {E : Type u_2} {m : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {ι : Type u_3} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι] {ℱ : Filtration ι m} [SigmaFiniteFiltration μ ℱ] {τ σ : Ω → WithTop ι} {f : ι → Ω → E} {n : ι} [Nonempty ι] (h : Martingale f ℱ μ) (hτ : IsStoppingTime ℱ τ) (hσ : IsStoppingTime ℱ σ) (hσ_le_τ : σ ≤ τ) (hτ_le : ∀ (x : Ω), τ x ≤ ↑n) (hτ_countable_range : (Set.range τ).Countable) (hσ_countable_range : (Set.range σ).Countable) [SigmaFinite (μ.trim ⋯)] :
stoppedValue f σ =ᶠ[ae μ] μ[stoppedValue f τ|hσ.measurableSpace]

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

source
theorem MeasureTheory.Martingale.stoppedValue_ae_eq_condExp_of_le {Ω : Type u_1} {E : Type u_2} {m : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {ι : Type u_3} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι] {ℱ : Filtration ι m} [SigmaFiniteFiltration μ ℱ] {τ σ : Ω → WithTop ι} {f : ι → Ω → E} {n : ι} [Nonempty ι] [Countable ι] (h : Martingale f ℱ μ) (hτ : IsStoppingTime ℱ τ) (hσ : IsStoppingTime ℱ σ) (hσ_le_τ : σ ≤ τ) (hτ_le : ∀ (x : Ω), τ x ≤ ↑n) [SigmaFinite (μ.trim ⋯)] :
stoppedValue f σ =ᶠ[ae μ] μ[stoppedValue f τ|hσ.measurableSpace]

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.

source
theorem MeasureTheory.Martingale.condExp_stoppedValue_stopping_time_ae_eq_restrict_le {Ω : Type u_1} {E : Type u_2} {m : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrder ι] [OrderBot ι] [TopologicalSpace ι] [DiscreteTopology ι] [MeasurableSpace ι] [BorelSpace ι] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] {ℱ : Filtration ι m} {τ σ : Ω → WithTop ι} {f : ι → Ω → E} {i : ι} (h : Martingale f ℱ μ) (hτ : IsStoppingTime ℱ τ) (hσ : IsStoppingTime ℱ σ) [SigmaFinite (μ.trim ⋯)] (hτ_le : ∀ (x : Ω), τ x ≤ ↑i) :
μ[stoppedValue f τ|hσ.measurableSpace] =ᶠ[ae (μ.restrict {x : Ω | τ x ≤ σ x})] stoppedValue f τ
source
theorem MeasureTheory.Martingale.stoppedValue_min_ae_eq_condExp {Ω : Type u_1} {E : Type u_2} {m : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {ι : Type u_3} [LinearOrder ι] [LocallyFiniteOrder ι] [OrderBot ι] [TopologicalSpace ι] [DiscreteTopology ι] [MeasurableSpace ι] [BorelSpace ι] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] {ℱ : Filtration ι m} {τ σ : Ω → WithTop ι} {f : ι → Ω → E} [SigmaFiniteFiltration μ ℱ] (h : Martingale f ℱ μ) (hτ : IsStoppingTime ℱ τ) (hσ : IsStoppingTime ℱ σ) {n : ι} (hτ_le : ∀ (x : Ω), τ x ≤ ↑n) [h_sf_min : SigmaFinite (μ.trim ⋯)] :
(stoppedValue f fun (x : Ω) => min (σ x) (τ x)) =ᶠ[ae μ] μ[stoppedValue f τ|hσ.measurableSpace]

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