English
For a martingale and a stopping time τ, the stopped value process evaluated at a stopping time τ is almost everywhere equal to the conditional expectation of f_n given the σ-algebra generated by τ, when restricted to events where τ equals a fixed i.
Русский
Для мартингала и останова τ процесс остановленного значения τ равен почти surely условному математическому ожиданию f_n относительно σ-алгебры, порождаемой τ, на событии {τ=i}.
LaTeX
$$$ \\text{stoppedValue}(f, \\tau) =_{\\mathrm{ae},\\; \\mu|_{\\{\\tau=i\\}}} \\mu[f_n \\mid h\\tau.meiasurableSpace] $$$
Lean4
theorem stoppedValue_ae_eq_restrict_eq (h : Martingale f ℱ μ) (hτ : IsStoppingTime ℱ τ) (hτ_le : ∀ x, τ x ≤ n)
[SigmaFinite (μ.trim (hτ.measurableSpace_le_of_le hτ_le))] (i : ι) :
stoppedValue f τ =ᵐ[μ.restrict {x | τ x = i}] μ[f n|hτ.measurableSpace] :=
by
refine Filter.EventuallyEq.trans ?_ (condExp_stopping_time_ae_eq_restrict_eq_const_of_le_const h hτ hτ_le i).symm
rw [Filter.EventuallyEq, ae_restrict_iff' (ℱ.le _ _ (hτ.measurableSet_eq i))]
refine Filter.Eventually.of_forall fun x hx => ?_
rw [Set.mem_setOf_eq] at hx
simp_rw [stoppedValue, hx]
