English
The integral over the full γ of density equals the mass κ a on univ × univ.
Русский
Интеграл плотности по всей γ равен массе κ a на (univ × univ).
LaTeX
$$∫ x, density κ ν a x s ∂(ν a) = (κ a).real (univ ×ˢ s)$$
Lean4
/-- Auxiliary lemma for `setIntegral_density`. -/
theorem setIntegral_density_of_measurableSet (hκν : fst κ ≤ ν) [IsFiniteKernel ν] (n : ℕ) (a : α) {s : Set β}
(hs : MeasurableSet s) {A : Set γ} (hA : MeasurableSet[countableFiltration γ n] A) :
∫ x in A, density κ ν a x s ∂(ν a) = (κ a).real (A ×ˢ s) :=
by
suffices ∫ x in A, density κ ν a x s ∂(ν a) = ∫ x in A, densityProcess κ ν n a x s ∂(ν a) by
exact this ▸ setIntegral_densityProcess hκν _ _ hs hA
suffices ∫ x in A, density κ ν a x s ∂(ν a) = limsup (fun i ↦ ∫ x in A, densityProcess κ ν i a x s ∂(ν a)) atTop
by
rw [this, ← limsup_const (α := ℕ) (f := atTop) (∫ x in A, densityProcess κ ν n a x s ∂(ν a)), limsup_congr]
simp only [eventually_atTop]
refine ⟨n, fun m hnm ↦ ?_⟩
rw [setIntegral_densityProcess_of_le hκν hnm _ hs hA, setIntegral_densityProcess hκν _ _ hs hA]
-- use L1 convergence
have h := tendsto_setIntegral_densityProcess hκν a hs A
rw [h.limsup_eq]
