English
If τ is a bounded stopping time and σ is another stopping time, then the value of a martingale at min{τ,σ} is almost surely equal to the conditional expectation of the martingale stopped at τ with respect to the σ-algebra generated by σ (the optional sampling theorem).
Русский
Если τ — ограниченное останова, а σ — другое останова, то значение мартингала в минимуме {τ,σ} почти surely равно условному ожиданию мартингала, остановленного в τ, по σ-алгебре (теорема об условной выборке).
LaTeX
$$$ \\text{stoppedValue}(f,\\min(σ,τ)) =_{\\mathrm{ae},\\mu} \\mu[ \\text{stoppedValue}(f,τ) \\mid h\\sigma.measurableSpace] $$$
Lean4
theorem condExp_stoppedValue_stopping_time_ae_eq_restrict_le (h : Martingale f ℱ μ) (hτ : IsStoppingTime ℱ τ)
(hσ : IsStoppingTime ℱ σ) [SigmaFinite (μ.trim hσ.measurableSpace_le)] (hτ_le : ∀ x, τ x ≤ i) :
μ[stoppedValue f τ|hσ.measurableSpace] =ᵐ[μ.restrict {x : Ω | τ x ≤ σ x}] stoppedValue f τ :=
by
rw [ae_eq_restrict_iff_indicator_ae_eq (hτ.measurableSpace_le _ (hτ.measurableSet_le_stopping_time hσ))]
refine
(condExp_indicator (integrable_stoppedValue ι hτ h.integrable hτ_le)
(hτ.measurableSet_stopping_time_le hσ)).symm.trans
?_
have h_int : Integrable ({ω : Ω | τ ω ≤ σ ω}.indicator (stoppedValue (fun n : ι => f n) τ)) μ :=
by
refine (integrable_stoppedValue ι hτ h.integrable hτ_le).indicator ?_
exact hτ.measurableSpace_le _ (hτ.measurableSet_le_stopping_time hσ)
have h_meas :
AEStronglyMeasurable[hσ.measurableSpace] ({ω : Ω | τ ω ≤ σ ω}.indicator (stoppedValue (fun n : ι => f n) τ)) μ :=
by
refine StronglyMeasurable.aestronglyMeasurable ?_
refine
StronglyMeasurable.stronglyMeasurable_of_measurableSpace_le_on (hτ.measurableSet_le_stopping_time hσ) ?_ ?_ ?_
· intro t ht
rw [Set.inter_comm _ t] at ht ⊢
rw [hτ.measurableSet_inter_le_iff hσ, IsStoppingTime.measurableSet_min_iff hτ hσ] at ht
exact ht.2
· refine StronglyMeasurable.indicator ?_ (hτ.measurableSet_le_stopping_time hσ)
refine Measurable.stronglyMeasurable ?_
exact measurable_stoppedValue h.adapted.progMeasurable_of_discrete hτ
· intro x hx
simp only [hx, Set.indicator_of_notMem, not_false_iff]
exact condExp_of_aestronglyMeasurable' hσ.measurableSpace_le h_meas h_int
