le_zero_of_predictable — Mathlib

English

A predictable martingale is almost surely equal to its initial value for all times.

Русский

Предсказуемый мартингал почти наверняка равен своему начальному значению на любом моменте времени.

LaTeX

$$$\\forall n, \\ f_n =^{\\text{ae}}_{μ} f_0$ under predictability (formally: Predictable martingale).$$$

Lean4

/-- A predictable supermartingale is a.e. less equal than its initial state. -/
theorem le_zero_of_predictable [Preorder E] [SigmaFiniteFiltration μ 𝒢] {f : ℕ → Ω → E} (hfmgle : Supermartingale f 𝒢 μ)
    (hfadp : Adapted 𝒢 fun n => f (n + 1)) (n : ℕ) : f n ≤ᵐ[μ] f 0 := by
  induction n with
  | zero => rfl
  | succ k ih =>
    exact
      ((Germ.coe_eq.mp <|
                congr_arg Germ.ofFun <|
                  condExp_of_stronglyMeasurable (𝒢.le _) (hfadp _) <| hfmgle.integrable _).symm.trans_le
            (hfmgle.2.1 k (k + 1) k.le_succ)).trans
        ih

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