English
A variant of the previous result: the process defined by summing ξ(k+1) · (f(k+1) − f(k)) over k is a Submartingale when ξ is adapted in a shifted way.
Русский
Вариант предыдущего результата: процесс, заданный суммированием ξ(k+1) · (f(k+1) − f(k)) по k, является субмартингал при условии адаптированности ξ сдвинуто.
LaTeX
$$$[IsFiniteMeasure \\ μ] \\Rightarrow \\text{Submartingale}\\Big( n \\mapsto \\sum_{k=0}^{n-1} ξ(k+1) (f(k+1) - f(k)) \\Big) 𝒢 μ.$$$
Lean4
/-- Given a discrete submartingale `f` and a predictable process `ξ` (i.e. `ξ (n + 1)` is adapted)
the process defined by `fun n => ∑ k ∈ Finset.range n, ξ (k + 1) * (f (k + 1) - f k)` is also a
submartingale. -/
theorem sum_mul_sub' [IsFiniteMeasure μ] {R : ℝ} {ξ f : ℕ → Ω → ℝ} (hf : Submartingale f 𝒢 μ)
(hξ : Adapted 𝒢 fun n => ξ (n + 1)) (hbdd : ∀ n ω, ξ n ω ≤ R) (hnonneg : ∀ n ω, 0 ≤ ξ n ω) :
Submartingale (fun n => ∑ k ∈ Finset.range n, ξ (k + 1) * (f (k + 1) - f k)) 𝒢 μ :=
hf.sum_mul_sub hξ (fun _ => hbdd _) fun _ => hnonneg _
