English
Under the same hypotheses as above, the process h_n = sum_{k=0}^{n-1} (1 − upcrossingStrat(a,b,f,N,k)) · (f(k+1) − f(k)) is a submartingale with respect to ℱ and μ.
Русский
При тех же предположениях утверждается, что процесс h_n = сумма_{k=0}^{n-1} (1 − upcrossingStrat(a,b,f,N,k)) · (f(k+1) − f(k)) образует субмартингал с отношением к ℱ и μ.
LaTeX
$$$h_n := \\sum_{k=0}^{n-1} (1-\\mathrm{upcrossingStrat}(a,b,f,N,k))\\,(f(k+1)-f(k)) \\quad\\Rightarrow\\quad h_n\\text{ is a submartingale w.r.t. }\\mathcal{F},\\mu.$$$
Lean4
theorem sum_sub_upcrossingStrat_mul [IsFiniteMeasure μ] (hf : Submartingale f ℱ μ) (a b : ℝ) (N : ℕ) :
Submartingale (fun n : ℕ => ∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) ℱ μ :=
by
refine
hf.sum_mul_sub (fun n => (adapted_const ℱ 1 n).sub (hf.adapted.upcrossingStrat_adapted n))
(?_ : ∀ n ω, (1 - upcrossingStrat a b f N n) ω ≤ 1) ?_
· exact fun n ω => sub_le_self _ upcrossingStrat_nonneg
· intro n ω
simp [upcrossingStrat_le_one]
