English
For any a and measurable s, the set-integral over A of density equals the real-value of κ a on A × s.
Русский
Для любого a и измеримого s интеграл по A плотности равен реальности κ a на A × s.
LaTeX
$$Tendsto (fun i => ∫ x in A, density κ ν i a x s ∂(ν a)) atTop (nhds ((κ a).real (univ ×ˢ s)))$$
Lean4
theorem tendsto_setIntegral_densityProcess (hκν : fst κ ≤ ν) [IsFiniteKernel ν] (a : α) {s : Set β}
(hs : MeasurableSet s) (A : Set γ) :
Tendsto (fun i ↦ ∫ x in A, densityProcess κ ν i a x s ∂(ν a)) atTop (𝓝 (∫ x in A, density κ ν a x s ∂(ν a))) :=
by
refine
tendsto_setIntegral_of_L1' (μ := ν a) (fun x ↦ density κ ν a x s) (integrable_density hκν a hs) (F := fun i x ↦
densityProcess κ ν i a x s) (l := atTop) (Eventually.of_forall (fun n ↦ integrable_densityProcess hκν _ _ hs)) ?_
A
refine (tendsto_congr fun n ↦ ?_).mp (tendsto_eLpNorm_one_densityProcess_limitProcess hκν a hs)
refine eLpNorm_congr_ae ?_
exact EventuallyEq.rfl.sub (density_ae_eq_limitProcess hκν a hs).symm
