# mathlib3documentation

probability.martingale.optional_sampling

# Optional sampling theorem #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 μ[stopped_value f τ | hσ.measurable_space].

## Main results #

• stopped_value_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 τ.
• stopped_value_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 σ.
• stopped_value_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 σ.
@[protected, instance]
theorem measure_theory.martingale.condexp_stopping_time_ae_eq_restrict_eq_const {Ω : Type u_1} {E : Type u_2} {m : measurable_space Ω} {μ : measure_theory.measure Ω} [ E] {ι : Type u_3} [linear_order ι] {ℱ : m} {τ : Ω ι} {f : ι Ω E} {i n : ι} (h : μ) (hτ : τ) [measure_theory.sigma_finite (μ.trim _)] (hin : i n) :
(f n) =ᵐ[μ.restrict {x : Ω | τ x = i}] f i
theorem measure_theory.martingale.condexp_stopping_time_ae_eq_restrict_eq_const_of_le_const {Ω : Type u_1} {E : Type u_2} {m : measurable_space Ω} {μ : measure_theory.measure Ω} [ E] {ι : Type u_3} [linear_order ι] {ℱ : m} {τ : Ω ι} {f : ι Ω E} {n : ι} (h : μ) (hτ : τ) (hτ_le : (x : Ω), τ x n) [measure_theory.sigma_finite (μ.trim _)] (i : ι) :
(f n) =ᵐ[μ.restrict {x : Ω | τ x = i}] f i
theorem measure_theory.martingale.stopped_value_ae_eq_restrict_eq {Ω : Type u_1} {E : Type u_2} {m : measurable_space Ω} {μ : measure_theory.measure Ω} [ E] {ι : Type u_3} [linear_order ι] {ℱ : m} {τ : Ω ι} {f : ι Ω E} {n : ι} (h : μ) (hτ : τ) (hτ_le : (x : Ω), τ x n) [measure_theory.sigma_finite (μ.trim _)] (i : ι) :
=ᵐ[μ.restrict {x : Ω | τ x = i}] (f n)
theorem measure_theory.martingale.stopped_value_ae_eq_condexp_of_le_const_of_countable_range {Ω : Type u_1} {E : Type u_2} {m : measurable_space Ω} {μ : measure_theory.measure Ω} [ E] {ι : Type u_3} [linear_order ι] {ℱ : m} {τ : Ω ι} {f : ι Ω E} {n : ι} (h : μ) (hτ : τ) (hτ_le : (x : Ω), τ x n) (h_countable_range : (set.range τ).countable) [measure_theory.sigma_finite (μ.trim _)] :

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 measure_theory.martingale.stopped_value_ae_eq_condexp_of_le_const {Ω : Type u_1} {E : Type u_2} {m : measurable_space Ω} {μ : measure_theory.measure Ω} [ E] {ι : Type u_3} [linear_order ι] {ℱ : m} {τ : Ω ι} {f : ι Ω E} {n : ι} [countable ι] (h : μ) (hτ : τ) (hτ_le : (x : Ω), τ x n) [measure_theory.sigma_finite (μ.trim _)] :

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 measure_theory.martingale.stopped_value_ae_eq_condexp_of_le_of_countable_range {Ω : Type u_1} {E : Type u_2} {m : measurable_space Ω} {μ : measure_theory.measure Ω} [ E] {ι : Type u_3} [linear_order ι] {ℱ : m} {τ σ : Ω ι} {f : ι Ω E} {n : ι} (h : μ) (hτ : τ) (hσ : σ) (hσ_le_τ : σ τ) (hτ_le : (x : Ω), τ x n) (hτ_countable_range : (set.range τ).countable) (hσ_countable_range : (set.range σ).countable) [measure_theory.sigma_finite (μ.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 measure_theory.martingale.stopped_value_ae_eq_condexp_of_le {Ω : Type u_1} {E : Type u_2} {m : measurable_space Ω} {μ : measure_theory.measure Ω} [ E] {ι : Type u_3} [linear_order ι] {ℱ : m} {τ σ : Ω ι} {f : ι Ω E} {n : ι} [countable ι] (h : μ) (hτ : τ) (hσ : σ) (hσ_le_τ : σ τ) (hτ_le : (x : Ω), τ x n) [measure_theory.sigma_finite (μ.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 [linear_order ι] [locally_finite_order ι] and [order_bot ι], 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 measure_theory.martingale.condexp_stopped_value_stopping_time_ae_eq_restrict_le {Ω : Type u_1} {E : Type u_2} {m : measurable_space Ω} {μ : measure_theory.measure Ω} [ E] {ι : Type u_3} [linear_order ι] [order_bot ι] [borel_space ι] [borel_space E] {ℱ : m} {τ σ : Ω ι} {f : ι Ω E} {n : ι} (h : μ) (hτ : τ) (hσ : σ) [measure_theory.sigma_finite (μ.trim _)] (hτ_le : (x : Ω), τ x n) :
=ᵐ[μ.restrict {x : Ω | τ x σ x}]
theorem measure_theory.martingale.stopped_value_min_ae_eq_condexp {Ω : Type u_1} {E : Type u_2} {m : measurable_space Ω} {μ : measure_theory.measure Ω} [ E] {ι : Type u_3} [linear_order ι] [order_bot ι] [borel_space ι] [borel_space E] {ℱ : m} {τ σ : Ω ι} {f : ι Ω E} (h : μ) (hτ : τ) (hσ : σ) {n : ι} (hτ_le : (x : Ω), τ x n) [h_sf_min : measure_theory.sigma_finite (μ.trim _)] :
(λ (x : Ω), linear_order.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 σ.