eq_zero_of_predictable — Mathlib

English

If f is a predictable martingale, then f_n = f_0 almost surely for all n.

Русский

Если f — предсказуемый мартингал, то f_n = f_0 почти наверняка для всех n.

LaTeX

$$$\\forall n, f_n =^{\\text{ae}}_{μ} f_0$ for predictable martingale.$$

Lean4

/-- A predictable martingale is a.e. equal to its initial state. -/
theorem eq_zero_of_predictable [SigmaFiniteFiltration μ 𝒢] {f : ℕ → Ω → E} (hfmgle : Martingale 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
            (hfmgle.2 k (k + 1) k.le_succ)).trans
        ih

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