English
If f is a submartingale, then the process formed by stoppedValue f at leastGE f r i is a submartingale.
Русский
Если f — субмартингал, то процесс, образованный остановленным значением stoppedValue f при leastGE f r i, является субмартингалом.
LaTeX
$$$\\text{Submartingale}(f, \\mathcal{F}, μ) \\Rightarrow \\text{Submartingale}(n \\mapsto \\text{stoppedValue}(f, \\text{leastGE} f r \\; n), \\mathcal{F}, μ).$$$
Lean4
theorem stoppedValue_leastGE [IsFiniteMeasure μ] (hf : Submartingale f ℱ μ) (r : ℝ) :
Submartingale (fun i => stoppedValue f (leastGE f r i)) ℱ μ :=
by
rw [submartingale_iff_expected_stoppedValue_mono]
· intro σ π hσ hπ hσ_le_π hπ_bdd
obtain ⟨n, hπ_le_n⟩ := hπ_bdd
simp_rw [stoppedValue_stoppedValue_leastGE f σ r fun i => (hσ_le_π i).trans (hπ_le_n i)]
simp_rw [stoppedValue_stoppedValue_leastGE f π r hπ_le_n]
refine hf.expected_stoppedValue_mono ?_ ?_ ?_ fun ω => (min_le_left _ _).trans (hπ_le_n ω)
· exact hσ.min (hf.adapted.isStoppingTime_leastGE _ _)
· exact hπ.min (hf.adapted.isStoppingTime_leastGE _ _)
· exact fun ω => min_le_min (hσ_le_π ω) le_rfl
·
exact fun i =>
stronglyMeasurable_stoppedValue_of_le hf.adapted.progMeasurable_of_discrete
(hf.adapted.isStoppingTime_leastGE _ _) leastGE_le
· exact fun i => integrable_stoppedValue _ (hf.adapted.isStoppingTime_leastGE _ _) hf.integrable leastGE_le
