English
If τ and σ are stopping times with σ ≤ τ and τ is bounded, the value at σ equals the conditional expectation of the value at τ given the σ-algebra of σ.
Русский
Если τ и σ — останова с σ ≤ τ и τ ограничено, то значение в σ равно условному ожиданию значения в τ относительно σ-алгебры σ.
LaTeX
$$$ \\text{stoppedValue}(f,\\sigma) =_{\\mathrm{ae},\\mu} \\mu[ \\text{stoppedValue}(f,τ) \\mid h\\sigma.measurableSpace] $$$
Lean4
/-- **Optional Sampling theorem**. If `τ` is a bounded stopping time and `σ` is another stopping
time, then the value of a martingale `f` at the stopping time `min τ σ` is almost everywhere equal
to the conditional expectation of `f` stopped at `τ` with respect to the σ-algebra generated
by `σ`. -/
theorem stoppedValue_min_ae_eq_condExp [SigmaFiniteFiltration μ ℱ] (h : Martingale f ℱ μ) (hτ : IsStoppingTime ℱ τ)
(hσ : IsStoppingTime ℱ σ) {n : ι} (hτ_le : ∀ x, τ x ≤ n)
[h_sf_min : SigmaFinite (μ.trim (hτ.min hσ).measurableSpace_le)] :
(stoppedValue f fun x => min (σ x) (τ x)) =ᵐ[μ] μ[stoppedValue f τ|hσ.measurableSpace] :=
by
refine (h.stoppedValue_ae_eq_condExp_of_le hτ (hσ.min hτ) (fun x => min_le_right _ _) hτ_le).trans ?_
refine ae_of_ae_restrict_of_ae_restrict_compl {x | σ x ≤ τ x} ?_ ?_
· exact condExp_min_stopping_time_ae_eq_restrict_le hσ hτ
· suffices
μ[stoppedValue f τ|(hσ.min hτ).measurableSpace] =ᵐ[μ.restrict {x | τ x ≤ σ x}]
μ[stoppedValue f τ|hσ.measurableSpace]
by
rw [ae_restrict_iff' (hσ.measurableSpace_le _ (hσ.measurableSet_le_stopping_time hτ).compl)]
rw [Filter.EventuallyEq, ae_restrict_iff'] at this
swap; · exact hτ.measurableSpace_le _ (hτ.measurableSet_le_stopping_time hσ)
filter_upwards [this] with x hx hx_mem
simp only [Set.mem_compl_iff, Set.mem_setOf_eq, not_le] at hx_mem
exact hx hx_mem.le
apply Filter.EventuallyEq.trans _ ((condExp_min_stopping_time_ae_eq_restrict_le hτ hσ).trans _)
· exact stoppedValue f τ
· rw [IsStoppingTime.measurableSpace_min hσ hτ, IsStoppingTime.measurableSpace_min hτ hσ, inf_comm]
· have h1 : μ[stoppedValue f τ|hτ.measurableSpace] = stoppedValue f τ :=
by
apply condExp_of_stronglyMeasurable hτ.measurableSpace_le
· exact Measurable.stronglyMeasurable <| measurable_stoppedValue h.adapted.progMeasurable_of_discrete hτ
· exact integrable_stoppedValue ι hτ h.integrable hτ_le
rw [h1]
exact (condExp_stoppedValue_stopping_time_ae_eq_restrict_le h hτ hσ hτ_le).symm
