English
If τ and σ are stopping times with a certain ordering and τ ≤ n, then the stopped value at σ equals the conditional expectation of the stopped value at τ with respect to the σ-algebra of σ, under countability hypotheses for the ranges.
Русский
Если τ и σ — останова с заданным порядком и τ ≤ n, то остановленное значение σ равно условному ожиданию остановленного значения τ по σ-алгебре σ, при счетности диапазонов.
LaTeX
$$$ \\text{stoppedValue}(f, \\sigma) =_{\\mathrm{ae},\\; \\mu} \\mu[\\text{stoppedValue}(f, \\tau) \\mid h\\sigma.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_of_countable_range (h : Martingale f ℱ μ) (hτ : IsStoppingTime ℱ τ)
(hτ_le : ∀ x, τ x ≤ n) (h_countable_range : (Set.range τ).Countable)
[SigmaFinite (μ.trim (hτ.measurableSpace_le_of_le hτ_le))] : stoppedValue f τ =ᵐ[μ] μ[f n|hτ.measurableSpace] :=
by
have : Set.univ = ⋃ i ∈ Set.range τ, {x | τ x = i} := by
ext1 x
simp only [Set.mem_univ, Set.mem_range, Set.iUnion_exists, Set.iUnion_iUnion_eq', Set.mem_iUnion, Set.mem_setOf_eq,
exists_apply_eq_apply']
nth_rw 1 [← @Measure.restrict_univ Ω _ μ]
rw [this, ae_eq_restrict_biUnion_iff _ h_countable_range]
exact fun i _ => stoppedValue_ae_eq_restrict_eq h _ hτ_le i
