martingale_const_fun — Mathlib

English

A constant function f(i) ≡ x with appropriate measurability and integrability conditions forms a martingale.

Русский

Пусть f(i) ≡ x; при надлежащей измеримости и интегрируемости это образует мартингейл.

LaTeX

$$$\\text{Martingale}(\\lambda i. x, \\mathcal{F}, \\mu)$$$

Lean4

theorem martingale_const_fun [OrderBot ι] (ℱ : Filtration ι m0) (μ : Measure Ω) [SigmaFiniteFiltration μ ℱ] {f : Ω → E}
    (hf : StronglyMeasurable[ℱ ⊥] f) (hfint : Integrable f μ) : Martingale (fun _ => f) ℱ μ :=
  by
  refine ⟨fun i => hf.mono <| ℱ.mono bot_le, fun i j _ => ?_⟩
  rw [condExp_of_stronglyMeasurable (ℱ.le _) (hf.mono <| ℱ.mono bot_le) hfint]

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