English
Let μ be a finite measure and f a real-valued submartingale adapted to a filtration ℱ. Then the process g_n defined by g_n = sum_{k=0}^{n-1} upcrossingStrat(a,b,f,N,k) · (f(k+1) − f(k)) is again a submartingale with respect to ℱ and μ.
Русский
Пусть μ — конечная мера и f — действительная произвольная субмартингейл относительно фильтрации ℱ. Тогда процесс g_n, заданный как g_n = сумма по k от 0 до n−1 [upcrossingStrat(a,b,f,N,k) · (f(k+1) − f(k))], является субмартингейлом относительно ℱ и μ.
LaTeX
$$$g_n := \\sum_{k=0}^{n-1} \\mathrm{upcrossingStrat}(a,b,f,N,k)\\,(f(k+1)-f(k))\\quad\\Rightarrow\\quad g_n\\text{ is a submartingale w.r.t. }\\mathcal{F},\\mu.$$$
Lean4
theorem sum_upcrossingStrat_mul [IsFiniteMeasure μ] (hf : Submartingale f ℱ μ) (a b : ℝ) (N : ℕ) :
Submartingale (fun n : ℕ => ∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)) ℱ μ :=
hf.sum_mul_sub hf.adapted.upcrossingStrat_adapted (fun _ _ => upcrossingStrat_le_one) fun _ _ =>
upcrossingStrat_nonneg
