memL1_limitProcess_densityProcess

English

The limit process (along the countable filtration) of the densityProcess sequence is in L1 with respect to ν a; i.e., it belongs to the L1 space.

Русский

Пределящий процесс плотностей по счетной фильтрации принадлежит пространству L1 относительно меры ν a.

LaTeX

$$MemLp ((countableFiltration γ).limitProcess (fun n x => densityProcess κ ν n a x s) (ν a)) 1 (ν a)$$

Lean4

theorem memL1_limitProcess_densityProcess (hκν : fst κ ≤ ν) [IsFiniteKernel ν] (a : α) {s : Set β}
    (hs : MeasurableSet s) :
    MemLp ((countableFiltration γ).limitProcess (fun n x ↦ densityProcess κ ν n a x s) (ν a)) 1 (ν a) :=
  by
  refine
    Submartingale.memLp_limitProcess (martingale_densityProcess hκν a hs).submartingale (R := (ν a univ).toNNReal)
      (fun n ↦ ?_)
  refine (eLpNorm_densityProcess_le hκν n a s).trans_eq ?_
  rw [ENNReal.coe_toNNReal]
  exact measure_ne_top _ _

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