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 martingalefat a stopping timeτbounded bynis the conditional expectation off nwith 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 martingalefatσ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 martingalefat the stopping timemin τ σis almost everywhere equal to the conditional expectation offstopped 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 Ω}
[normed_add_comm_group E]
[normed_space ℝ E]
[complete_space E]
{ι : Type u_3}
[linear_order ι]
[topological_space ι]
[order_topology ι]
[topological_space.first_countable_topology ι]
{ℱ : measure_theory.filtration ι m}
[measure_theory.sigma_finite_filtration μ ℱ]
{τ : Ω → ι}
{f : ι → Ω → E}
{i n : ι}
[filter.at_top.is_countably_generated]
(h : measure_theory.martingale f ℱ μ)
(hτ : measure_theory.is_stopping_time ℱ τ)
[measure_theory.sigma_finite (μ.trim _)]
(hin : i ≤ n) :
measure_theory.condexp hτ.measurable_space μ (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 Ω}
[normed_add_comm_group E]
[normed_space ℝ E]
[complete_space E]
{ι : Type u_3}
[linear_order ι]
[topological_space ι]
[order_topology ι]
[topological_space.first_countable_topology ι]
{ℱ : measure_theory.filtration ι m}
[measure_theory.sigma_finite_filtration μ ℱ]
{τ : Ω → ι}
{f : ι → Ω → E}
{n : ι}
(h : measure_theory.martingale f ℱ μ)
(hτ : measure_theory.is_stopping_time ℱ τ)
(hτ_le : ∀ (x : Ω), τ x ≤ n)
[measure_theory.sigma_finite (μ.trim _)]
(i : ι) :
measure_theory.condexp hτ.measurable_space μ (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 Ω}
[normed_add_comm_group E]
[normed_space ℝ E]
[complete_space E]
{ι : Type u_3}
[linear_order ι]
[topological_space ι]
[order_topology ι]
[topological_space.first_countable_topology ι]
{ℱ : measure_theory.filtration ι m}
[measure_theory.sigma_finite_filtration μ ℱ]
{τ : Ω → ι}
{f : ι → Ω → E}
{n : ι}
(h : measure_theory.martingale f ℱ μ)
(hτ : measure_theory.is_stopping_time ℱ τ)
(hτ_le : ∀ (x : Ω), τ x ≤ n)
[measure_theory.sigma_finite (μ.trim _)]
(i : ι) :
measure_theory.stopped_value f τ =ᵐ[μ.restrict {x : Ω | τ x = i}] measure_theory.condexp hτ.measurable_space μ (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 Ω}
[normed_add_comm_group E]
[normed_space ℝ E]
[complete_space E]
{ι : Type u_3}
[linear_order ι]
[topological_space ι]
[order_topology ι]
[topological_space.first_countable_topology ι]
{ℱ : measure_theory.filtration ι m}
[measure_theory.sigma_finite_filtration μ ℱ]
{τ : Ω → ι}
{f : ι → Ω → E}
{n : ι}
(h : measure_theory.martingale f ℱ μ)
(hτ : measure_theory.is_stopping_time ℱ τ)
(hτ_le : ∀ (x : Ω), τ x ≤ n)
(h_countable_range : (set.range τ).countable)
[measure_theory.sigma_finite (μ.trim _)] :
measure_theory.stopped_value f τ =ᵐ[μ] measure_theory.condexp hτ.measurable_space μ (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
measure_theory.martingale.stopped_value_ae_eq_condexp_of_le_const
{Ω : Type u_1}
{E : Type u_2}
{m : measurable_space Ω}
{μ : measure_theory.measure Ω}
[normed_add_comm_group E]
[normed_space ℝ E]
[complete_space E]
{ι : Type u_3}
[linear_order ι]
[topological_space ι]
[order_topology ι]
[topological_space.first_countable_topology ι]
{ℱ : measure_theory.filtration ι m}
[measure_theory.sigma_finite_filtration μ ℱ]
{τ : Ω → ι}
{f : ι → Ω → E}
{n : ι}
[countable ι]
(h : measure_theory.martingale f ℱ μ)
(hτ : measure_theory.is_stopping_time ℱ τ)
(hτ_le : ∀ (x : Ω), τ x ≤ n)
[measure_theory.sigma_finite (μ.trim _)] :
measure_theory.stopped_value f τ =ᵐ[μ] measure_theory.condexp hτ.measurable_space μ (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
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 Ω}
[normed_add_comm_group E]
[normed_space ℝ E]
[complete_space E]
{ι : Type u_3}
[linear_order ι]
[topological_space ι]
[order_topology ι]
[topological_space.first_countable_topology ι]
{ℱ : measure_theory.filtration ι m}
[measure_theory.sigma_finite_filtration μ ℱ]
{τ σ : Ω → ι}
{f : ι → Ω → E}
{n : ι}
(h : measure_theory.martingale f ℱ μ)
(hτ : measure_theory.is_stopping_time ℱ τ)
(hσ : measure_theory.is_stopping_time ℱ σ)
(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 Ω}
[normed_add_comm_group E]
[normed_space ℝ E]
[complete_space E]
{ι : Type u_3}
[linear_order ι]
[topological_space ι]
[order_topology ι]
[topological_space.first_countable_topology ι]
{ℱ : measure_theory.filtration ι m}
[measure_theory.sigma_finite_filtration μ ℱ]
{τ σ : Ω → ι}
{f : ι → Ω → E}
{n : ι}
[countable ι]
(h : measure_theory.martingale f ℱ μ)
(hτ : measure_theory.is_stopping_time ℱ τ)
(hσ : measure_theory.is_stopping_time ℱ σ)
(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 Ω}
[normed_add_comm_group E]
[normed_space ℝ E]
[complete_space E]
{ι : Type u_3}
[linear_order ι]
[locally_finite_order ι]
[order_bot ι]
[topological_space ι]
[discrete_topology ι]
[measurable_space ι]
[borel_space ι]
[measurable_space E]
[borel_space E]
[topological_space.second_countable_topology E]
{ℱ : measure_theory.filtration ι m}
{τ σ : Ω → ι}
{f : ι → Ω → E}
{n : ι}
(h : measure_theory.martingale f ℱ μ)
(hτ : measure_theory.is_stopping_time ℱ τ)
(hσ : measure_theory.is_stopping_time ℱ σ)
[measure_theory.sigma_finite (μ.trim _)]
(hτ_le : ∀ (x : Ω), τ x ≤ n) :
measure_theory.condexp hσ.measurable_space μ (measure_theory.stopped_value f τ) =ᵐ[μ.restrict {x : Ω | τ x ≤ σ x}] measure_theory.stopped_value f τ
theorem
measure_theory.martingale.stopped_value_min_ae_eq_condexp
{Ω : Type u_1}
{E : Type u_2}
{m : measurable_space Ω}
{μ : measure_theory.measure Ω}
[normed_add_comm_group E]
[normed_space ℝ E]
[complete_space E]
{ι : Type u_3}
[linear_order ι]
[locally_finite_order ι]
[order_bot ι]
[topological_space ι]
[discrete_topology ι]
[measurable_space ι]
[borel_space ι]
[measurable_space E]
[borel_space E]
[topological_space.second_countable_topology E]
{ℱ : measure_theory.filtration ι m}
{τ σ : Ω → ι}
{f : ι → Ω → E}
[measure_theory.sigma_finite_filtration μ ℱ]
(h : measure_theory.martingale f ℱ μ)
(hτ : measure_theory.is_stopping_time ℱ τ)
(hσ : measure_theory.is_stopping_time ℱ σ)
{n : ι}
(hτ_le : ∀ (x : Ω), τ x ≤ n)
[h_sf_min : measure_theory.sigma_finite (μ.trim _)] :
measure_theory.stopped_value f (λ (x : Ω), linear_order.min (σ x) (τ x)) =ᵐ[μ] measure_theory.condexp hσ.measurable_space μ (measure_theory.stopped_value 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 σ.