English
Given a finite measure μ, a Submartingale f and a predictable ξ with certain boundedness, the process defined by the finite sum of ξ_k · (f(k+1) − f(k)) is a Submartingale with respect to the same filtration and μ.
Русский
При наличии конечной меры μ, субмартингал f и предсказуемый ξ с некоторыми ограничениями, процесс, заданный суммой по k от ξ_k · (f(k+1) − f(k)), является субмартингалом.
LaTeX
$$$[IsFiniteMeasure \\ μ] \\Rightarrow \\text{Submartingale}\\Big( n \\mapsto \\sum_{k=0}^{n-1} ξ_k (f(k+1) - f(k)) \\Big) \\ 𝒢 \\ μ.$$$
Lean4
theorem sum_mul_sub [IsFiniteMeasure μ] {R : ℝ} {ξ f : ℕ → Ω → ℝ} (hf : Submartingale f 𝒢 μ) (hξ : Adapted 𝒢 ξ)
(hbdd : ∀ n ω, ξ n ω ≤ R) (hnonneg : ∀ n ω, 0 ≤ ξ n ω) :
Submartingale (fun n => ∑ k ∈ Finset.range n, ξ k * (f (k + 1) - f k)) 𝒢 μ :=
by
have hξbdd : ∀ i, ∃ C, ∀ ω, |ξ i ω| ≤ C := fun i => ⟨R, fun ω => (abs_of_nonneg (hnonneg i ω)).trans_le (hbdd i ω)⟩
have hint : ∀ m, Integrable (∑ k ∈ Finset.range m, ξ k * (f (k + 1) - f k)) μ := fun m =>
integrable_finset_sum' _ fun i _ =>
Integrable.bdd_mul ((hf.integrable _).sub (hf.integrable _)) hξ.stronglyMeasurable.aestronglyMeasurable (hξbdd _)
have hadp : Adapted 𝒢 fun n => ∑ k ∈ Finset.range n, ξ k * (f (k + 1) - f k) :=
by
intro m
refine Finset.stronglyMeasurable_sum _ fun i hi => ?_
rw [Finset.mem_range] at hi
exact
(hξ.stronglyMeasurable_le hi.le).mul
((hf.adapted.stronglyMeasurable_le (Nat.succ_le_of_lt hi)).sub (hf.adapted.stronglyMeasurable_le hi.le))
refine submartingale_of_condExp_sub_nonneg_nat hadp hint fun i => ?_
simp only [← Finset.sum_Ico_eq_sub _ (Nat.le_succ _), Nat.Ico_succ_singleton, Finset.sum_singleton]
exact
EventuallyLE.trans
(EventuallyLE.mul_nonneg (Eventually.of_forall (hnonneg _)) (hf.condExp_sub_nonneg (Nat.le_succ _)))
(condExp_mul_of_stronglyMeasurable_left (hξ _)
(((hf.integrable _).sub (hf.integrable _)).bdd_mul hξ.stronglyMeasurable.aestronglyMeasurable (hξbdd _))
((hf.integrable _).sub (hf.integrable _))).symm.le
