process — Mathlib

English

The martingale part and the predictable part sum to the original process; their sum equals f.

Русский

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

LaTeX

$$$$\mathrm{martingalePart}(f, \mathcal{F}, \mu) + \mathrm{predictablePart}(f, \mathcal{F}, \mu) = f.$$$$

Lean4

/-- Auxiliary definition required to prove Lévy's generalization of the Borel-Cantelli lemmas for
which we will take the martingale part. -/
noncomputable def process (s : ℕ → Set Ω) (n : ℕ) : Ω → ℝ :=
  ∑ k ∈ Finset.range n, (s (k + 1)).indicator 1

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