smul — Mathlib

English

Repeatedly, scaling of martingales preserves martingale property.

Русский

Повторно масштабирование мартингалов сохраняет свойство мартингала.

LaTeX

$$$\\text{smul}(c, \\text{Martingale}(f, \\mathcal{F}, \\mu))$$$

Lean4

theorem smul (c : ℝ) (hf : Martingale f ℱ μ) : Martingale (c • f) ℱ μ :=
  by
  refine ⟨hf.adapted.smul c, fun i j hij => ?_⟩
  refine (condExp_smul ..).trans ((hf.2 i j hij).mono fun x hx => ?_)
  simp only [Pi.smul_apply, hx]

Похожие утверждения