English
If τ and σ are stopping times with σ ≤ τ and τ is bounded, then the stopped value at σ equals the conditional expectation of the stopped value at τ with respect to the σ-algebra of σ.
Русский
Если τ и σ — останова, причём σ ≤ τ, а τ ограничено, то остановленное значение σ равно условному ожиданию остановленного значения τ по σ-алгебре σ.
LaTeX
$$$ \\text{stoppedValue}(f,\\sigma) =_{\\mathrm{ae}, \\mu} \\mu[ \\text{stoppedValue}(f, \\tau) \\mid h\\sigma.measurableSpace] $$$
Lean4
/-- If `τ` and `σ` are two stopping times with `σ ≤ τ` and `τ` is bounded, then the value of a
martingale `f` at `σ` is the conditional expectation of its value at `τ` with respect to the
σ-algebra generated by `σ`. -/
theorem stoppedValue_ae_eq_condExp_of_le [Countable ι] (h : Martingale f ℱ μ) (hτ : IsStoppingTime ℱ τ)
(hσ : IsStoppingTime ℱ σ) (hσ_le_τ : σ ≤ τ) (hτ_le : ∀ x, τ x ≤ n) [SigmaFinite (μ.trim hσ.measurableSpace_le)] :
stoppedValue f σ =ᵐ[μ] μ[stoppedValue f τ|hσ.measurableSpace] :=
h.stoppedValue_ae_eq_condExp_of_le_of_countable_range hτ hσ hσ_le_τ hτ_le (Set.to_countable _) (Set.to_countable _)
