English
If the range of τ is countable, the stopped value at τ is almost everywhere equal to the conditional expectation of the stopped value at another time, conditioning on the σ-algebra generated by τ.
Русский
Если образ τ конечен по счету (счетно), остановленное значение τ равно почти surely условному ожиданию остановленного значения τ при другом времени, по σ-алгебре, соответствующей τ.
LaTeX
$$$ \\text{stoppedValue}(f,\\tau) =_{\\mathrm{ae},\\mu} \\mu[ \\text{stoppedValue}(f, \\tau') \\mid h\\tau.measurableSpace] $$$
Lean4
/-- The value of a martingale `f` at a stopping time `τ` bounded by `n` is the conditional
expectation of `f n` with respect to the σ-algebra generated by `τ`. -/
theorem stoppedValue_ae_eq_condExp_of_le_const [Countable ι] (h : Martingale f ℱ μ) (hτ : IsStoppingTime ℱ τ)
(hτ_le : ∀ x, τ x ≤ n) [SigmaFinite (μ.trim (hτ.measurableSpace_le_of_le hτ_le))] :
stoppedValue f τ =ᵐ[μ] μ[f n|hτ.measurableSpace] :=
h.stoppedValue_ae_eq_condExp_of_le_const_of_countable_range hτ hτ_le (Set.to_countable _)
