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 _ _