English
If τ ≤ σ, then the stopped value at σ is the conditional expectation of the stopped value at τ w.r.t. σ's σ-algebra; in particular, if σ ≤ τ, the equality holds on the restricted set {σ ≤ τ}.
Русский
Если τ ≤ σ, то остановленное значение τ эквивалентно условному ожиданию остановленного значения τ по σ-алгебре σ; в частности, если σ ≤ τ, равенство выполняется на {σ ≤ τ}.
LaTeX
$$$ \\text{stoppedValue}(f,\\tau) =_{\\mathrm{ae}, \\mu|_{\\{\\tau ≤ σ\\}}} \\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_of_countable_range (h : Martingale f ℱ μ) (hτ : IsStoppingTime ℱ τ)
(hσ : IsStoppingTime ℱ σ) (hσ_le_τ : σ ≤ τ) (hτ_le : ∀ x, τ x ≤ n) (hτ_countable_range : (Set.range τ).Countable)
(hσ_countable_range : (Set.range σ).Countable)
[SigmaFinite (μ.trim (hσ.measurableSpace_le_of_le fun x => (hσ_le_τ x).trans (hτ_le x)))] :
stoppedValue f σ =ᵐ[μ] μ[stoppedValue f τ|hσ.measurableSpace] :=
by
have : SigmaFinite (μ.trim (hτ.measurableSpace_le_of_le hτ_le)) :=
sigmaFiniteTrim_mono _ (IsStoppingTime.measurableSpace_mono hσ hτ hσ_le_τ)
have : μ[stoppedValue f τ|hσ.measurableSpace] =ᵐ[μ] μ[μ[f n|hτ.measurableSpace]|hσ.measurableSpace] :=
condExp_congr_ae (h.stoppedValue_ae_eq_condExp_of_le_const_of_countable_range hτ hτ_le hτ_countable_range)
refine
(Filter.EventuallyEq.trans ?_ (condExp_condExp_of_le ?_ (hτ.measurableSpace_le_of_le hτ_le)).symm).trans this.symm
·
exact
h.stoppedValue_ae_eq_condExp_of_le_const_of_countable_range hσ (fun x => (hσ_le_τ x).trans (hτ_le x))
hσ_countable_range
· exact hσ.measurableSpace_mono hτ hσ_le_τ
