English
Under the same hypotheses as the previous result, but with a constaint capturing τ ≤ n via hτ_le, the same restriction equality holds: the conditional expectation of f_n given the σ-algebra of τ equals f_i almost surely on {τ = i}.
Русский
При тех же предположениях, дополнительно с ограничением τ ≤ n через hτ_le, выполняется тот же вид равенства условного ожидания: μ[f_n | 𝓕_τ] = a.e. 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_of_le_const (h : Martingale f ℱ μ) (hτ : IsStoppingTime ℱ τ)
(hτ_le : ∀ x, τ x ≤ n) [SigmaFinite (μ.trim (hτ.measurableSpace_le_of_le hτ_le))] (i : ι) :
μ[f n|hτ.measurableSpace] =ᵐ[μ.restrict {x | τ x = i}] f i :=
by
by_cases hin : i ≤ n
· 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_of_le hτ_le) (ℱ.le i)
(hτ.measurableSet_eq' i) fun t => ?_
rw [Set.inter_comm _ t, IsStoppingTime.measurableSet_inter_eq_iff]
· suffices {x : Ω | τ x = i} = ∅ by simp [this]; norm_cast
ext1 x
simp only [Set.mem_setOf_eq, Set.mem_empty_iff_false, iff_false]
rintro rfl
exact hin (hτ_le x)
