English
Let f be a martingale with respect to a filtration. For a stopping time τ and an index i with i ≤ n, the conditional expectation of f at time n given the σ-algebra generated by τ equals the value f(i) almost everywhere on the event {τ = i}.
Русский
Пусть f — мартингал относительно фильтрации. Для останова τ и индекса i с i ≤ n условное математическое ожидание f_n при условии σ-алгебры, порождаемой τ, равно значению f_i почти наверняка на событии {τ = i}.
LaTeX
$$$ \\mu[f_n \\mid \\mathcal{F}_\\tau] =_{\\mathrm{ae},\\; \\mu|_{\\{\\tau=i\\}}} f_i $$$
Lean4
theorem condExp_stopping_time_ae_eq_restrict_eq_const [(Filter.atTop : Filter ι).IsCountablyGenerated]
(h : Martingale f ℱ μ) (hτ : IsStoppingTime ℱ τ) [SigmaFinite (μ.trim hτ.measurableSpace_le)] (hin : i ≤ n) :
μ[f n|hτ.measurableSpace] =ᵐ[μ.restrict {x | τ x = i}] f i :=
by
refine Filter.EventuallyEq.trans ?_ (ae_restrict_of_ae (h.condExp_ae_eq hin))
refine
condExp_ae_eq_restrict_of_measurableSpace_eq_on hτ.measurableSpace_le (ℱ.le i) (hτ.measurableSet_eq' i) fun t => ?_
rw [Set.inter_comm _ t, IsStoppingTime.measurableSet_inter_eq_iff]
