tendsto_eLpNorm_one_restrict_densityProcess_limitProcess

English

The L1 distance between the densityProcess sequence and its limitProcess converges to zero in eLp-norm almost surely; i.e., the eLp-norm tends to zero along atTop.

Русский

Расстояние в eLp-норме между последовательностью densityProcess и её пределом сходится к нулю почти surely; т.е. eLpNorm→0 при tendsto к бесконечности.

LaTeX

$$Tendsto (fun n ↦ eLpNorm ((fun x ↦ densityProcess κ ν n a x s) - (countableFiltration γ).limitProcess (fun n x ↦ densityProcess κ ν n a x s) (ν a)) 1 (ν a)) atTop (nhds 0)$$

Lean4

theorem tendsto_eLpNorm_one_restrict_densityProcess_limitProcess [IsFiniteKernel ν] (hκν : fst κ ≤ ν) (a : α)
    {s : Set β} (hs : MeasurableSet s) (A : Set γ) :
    Tendsto
      (fun n ↦
        eLpNorm
          ((fun x ↦ densityProcess κ ν n a x s) -
            (countableFiltration γ).limitProcess (fun n x ↦ densityProcess κ ν n a x s) (ν a))
          1 ((ν a).restrict A))
      atTop (𝓝 0) :=
  tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds
    (tendsto_eLpNorm_one_densityProcess_limitProcess hκν a hs) (fun _ ↦ zero_le') (fun _ ↦ eLpNorm_restrict_le _ _ _ _)

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