density_ae_eq_limitProcess — Mathlib

English

Convergence of the densityProcess sequence to a limit process holds under finiteness of ν and finite kernels; the limit process is the one given by limitProcess.

Русский

Сходимость последовательности densityProcess к пределу выполняется при конечности ν и конечных ядрах; предел задаётся как limitProcess.

LaTeX

$$Tendsto (fun n ↦ density κ ν n a x s) atTop (nhds ((countableFiltration γ).limitProcess (fun n x ↦ densityProcess κ ν n a x s) (ν a)) x)$$

Lean4

theorem density_ae_eq_limitProcess (hκν : fst κ ≤ ν) [IsFiniteKernel ν] (a : α) {s : Set β} (hs : MeasurableSet s) :
    (fun x ↦ density κ ν a x s) =ᵐ[ν a]
      (countableFiltration γ).limitProcess (fun n x ↦ densityProcess κ ν n a x s) (ν a) :=
  by filter_upwards [tendsto_densityProcess_limitProcess hκν a hs] with t ht using ht.limsup_eq

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