tendsto_m_density — Mathlib

English

There is almost sure convergence of the densityProcess to the density κ ν a x s, i.e., the density equals the limit of the process almost surely.

Русский

Существует почти наверняка совпадение плотности density κ ν a x s с пределом процесса density.

LaTeX

$$Tendsto (fun n ↦ density κ ν n a x s) atTop (nhds (density κ ν a x s))$$

Lean4

theorem tendsto_m_density (hκν : fst κ ≤ ν) (a : α) [IsFiniteKernel ν] {s : Set β} (hs : MeasurableSet s) :
    ∀ᵐ x ∂(ν a), Tendsto (fun n ↦ densityProcess κ ν n a x s) atTop (𝓝 (density κ ν a x s)) := by
  filter_upwards [tendsto_densityProcess_limitProcess hκν a hs, density_ae_eq_limitProcess hκν a hs] with t h1 h2 using
    h2 ▸ h1

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