process_difference_le — Mathlib

English

The martingale part and the predictable part add up to the original process; their sum recovers f.

Русский

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

LaTeX

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

Lean4

theorem process_difference_le (s : ℕ → Set Ω) (ω : Ω) (n : ℕ) : |process s (n + 1) ω - process s n ω| ≤ (1 : ℝ≥0) :=
  by
  norm_cast
  rw [process, process, Finset.sum_apply, Finset.sum_apply, Finset.sum_range_succ_sub_sum, ← Real.norm_eq_abs,
    norm_indicator_eq_indicator_norm]
  refine Set.indicator_le' (fun _ _ => ?_) (fun _ _ => zero_le_one) _
  rw [Pi.one_apply, norm_one]

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