ae_not_tendsto_atTop_atBot — Mathlib

English

Decompose any square-integrable stochastic process into a martingale part and a predictable part, with the original process equal to the sum of these two parts.

Русский

Любой процесс с конечной второй моментной равен сумме маргинального (мартингальной) и предсказуемой части.

LaTeX

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

Lean4

theorem ae_not_tendsto_atTop_atBot [IsFiniteMeasure μ] (hf : Martingale f ℱ μ)
    (hbdd : ∀ᵐ ω ∂μ, ∀ i, |f (i + 1) ω - f i ω| ≤ R) : ∀ᵐ ω ∂μ, ¬Tendsto (fun n => f n ω) atTop atBot := by
  filter_upwards [hf.bddAbove_range_iff_bddBelow_range hbdd] with ω hω htop using
    not_bddBelow_of_tendsto_atBot htop (hω.1 <| bddAbove_range_of_tendsto_atTop_atBot htop)

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