condExp_stopping_time_ae_eq_restrict_eq_of_countable

English

If the stopping time range is countable, the same ae-equality of conditional expectations holds for each i when restricting to the event {τ = i}.

Русский

Если диапазон времени остановки счетный, то та же ae-эквалентность условного ожидания справедлива на каждом событии {τ=i}.

LaTeX

$$$\forall (hτ : IsStoppingTime ℱ τ)(h_countable : (Set.range τ).Countable) [SigmaFinite (μ.trim (hτ.measurableSpace_le_of_countable_range h_countable))] (i : ι),\ (μ|{x|τ x=i}) f = μ[f|ℱ i] \text{ a.e.}$$$

Lean4

theorem condExp_stopping_time_ae_eq_restrict_eq_of_countable [Countable ι] [SigmaFiniteFiltration μ ℱ]
    (hτ : IsStoppingTime ℱ τ) [SigmaFinite (μ.trim hτ.measurableSpace_le_of_countable)] (i : ι) :
    μ[f|hτ.measurableSpace] =ᵐ[μ.restrict {x | τ x = i}] μ[f|ℱ i] :=
  condExp_stopping_time_ae_eq_restrict_eq_of_countable_range hτ (Set.to_countable _) i

Похожие утверждения