English
For an antitone seq of sets under the finite kernel framework, the same limit-to-zero result holds, reinforcing convergence behavior of density processes.
Русский
Для антитонической последовательности множеств в рамках конечного ядра аналогично утверждение о сходящемся к нулю пределе плотностей.
LaTeX
$$$\lim_{m\to\infty} \densityProcess κ ν n a x (seq m) = 0$$$
Lean4
theorem tendsto_eLpNorm_one_densityProcess_limitProcess (hκν : fst κ ≤ ν) [IsFiniteKernel ν] (a : α) {s : Set β}
(hs : MeasurableSet s) :
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 (𝓝 0) :=
by
refine Submartingale.tendsto_eLpNorm_one_limitProcess ?_ ?_
· exact (martingale_densityProcess hκν a hs).submartingale
· refine uniformIntegrable_of le_rfl ENNReal.one_ne_top ?_ ?_
· exact fun n ↦ (measurable_densityProcess_right κ ν n a hs).aestronglyMeasurable
· refine fun ε _ ↦ ⟨2, fun n ↦ le_of_eq_of_le ?_ (?_ : 0 ≤ ENNReal.ofReal ε)⟩
· suffices {x | 2 ≤ ‖densityProcess κ ν n a x s‖₊} = ∅ by simp [this]
ext x
simp only [mem_setOf_eq, mem_empty_iff_false, iff_false, not_le]
refine (?_ : _ ≤ (1 : ℝ≥0)).trans_lt one_lt_two
rw [Real.nnnorm_of_nonneg (densityProcess_nonneg _ _ _ _ _ _)]
exact mod_cast (densityProcess_le_one hκν _ _ _ _)
· simp
