English
Let τ be a stopping time for filtration ℱ with a countable range for time index; then the conditional expectation of f given hτ.measurableSpace is ae-equal to the conditional expectation given ℱ i under the restriction to τ x = i, for each i in the range.
Русский
Пусть τ — остановка для фильтрации ℱ с счетной областью значений времени; тогда условное ожидание f с учётом пространства τ эквивалентно условному ожиданию по ℱ i на ограничении τ x = i, для каждого i.
LaTeX
$$$\forall (hτ : IsStoppingTime ℱ τ)(h_countable : (Set.range τ).Countable) [SigmaFinite (μ.trim (hτ.measurableSpace_le_of_countable_range h_countable))] (i : ι),\ μ[f|hτ.measurableSpace] =ᵐ[μ.restrict {x | τ x = i}] μ[f|ℱ i]$$$
Lean4
theorem condExp_stopping_time_ae_eq_restrict_eq_of_countable_range [SigmaFiniteFiltration μ ℱ] (hτ : IsStoppingTime ℱ τ)
(h_countable : (Set.range τ).Countable)
[SigmaFinite (μ.trim (hτ.measurableSpace_le_of_countable_range h_countable))] (i : ι) :
μ[f|hτ.measurableSpace] =ᵐ[μ.restrict {x | τ x = i}] μ[f|ℱ i] :=
by
refine
condExp_ae_eq_restrict_of_measurableSpace_eq_on (hτ.measurableSpace_le_of_countable_range h_countable) (ℱ.le i)
(hτ.measurableSet_eq_of_countable_range' h_countable i) fun t => ?_
rw [Set.inter_comm _ t, IsStoppingTime.measurableSet_inter_eq_iff]
