integrable_martingalePart — Mathlib

English

If every f_n is integrable with respect to μ, then the martingalePart(f, F, μ)_n is integrable for every n.

Русский

Если каждый f_n интегрируем по μ, то для всех n интегрируемость мартингальной части f по отношению к F и μ сохраняется: интеграл манифеста мартингальной части конечен.

LaTeX

$$$\\forall n\\, \\operatorname{Integrable}(\\mathrm{martingalePart}(f,\\mathcal{F},\\mu)_{n}, \\mu).$$$

Lean4

theorem integrable_martingalePart (hf_int : ∀ n, Integrable (f n) μ) (n : ℕ) : Integrable (martingalePart f ℱ μ n) μ :=
  by
  rw [martingalePart_eq_sum]
  fun_prop

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