English
For a fixed a ∈ α and measurable s ⊆ β, there is almost everywhere convergence in x ∈ γ of densityProcess κ ν n a x s to a limitProcess value as n → ∞; this limit is the limitProcess of the density processes along the countable filtration.
Русский
Для фиксированного a и измеримого s ⊆ β существует почти везде по x ∈ γ сходение плотности densityProcess κ ν n a x s к пределу, который является limitProcess плотностей вдоль счетной фильтрации.
LaTeX
$$\forall a, s, hs, ∀ᵐ x ∂(ν a), Tendsto (fun n ↦ densityProcess κ ν n a x s) atTop (nhds ( (countableFiltration γ).limitProcess (fun n x ↦ densityProcess κ ν n a x s) (ν a) x ))$$
Lean4
theorem tendsto_densityProcess_limitProcess (hκν : fst κ ≤ ν) [IsFiniteKernel ν] (a : α) {s : Set β}
(hs : MeasurableSet s) :
∀ᵐ x ∂(ν a),
Tendsto (fun n ↦ densityProcess κ ν n a x s) atTop
(𝓝 ((countableFiltration γ).limitProcess (fun n x ↦ densityProcess κ ν n a x s) (ν a) x)) :=
by
refine
Submartingale.ae_tendsto_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 _ _
