setLIntegral_density — Mathlib

English

For κ and ν and fixed a, the map x ↦ density κ ν a x s is measurable for any measurable s.

Русский

Для κ и ν и фиксированного a отображение x ↦ density κ ν a x s измеримо.

LaTeX

$$Measurable (fun x => density κ ν a x s)$$

Lean4

theorem setLIntegral_density (hκν : fst κ ≤ ν) [IsFiniteKernel ν] (a : α) {s : Set β} (hs : MeasurableSet s) {A : Set γ}
    (hA : MeasurableSet A) : ∫⁻ x in A, ENNReal.ofReal (density κ ν a x s) ∂(ν a) = κ a (A ×ˢ s) :=
  by
  have : IsFiniteKernel κ := isFiniteKernel_of_isFiniteKernel_fst (h := isFiniteKernel_of_le hκν)
  rw [← ofReal_integral_eq_lintegral_ofReal]
  · rw [setIntegral_density hκν a hs hA, measureReal_def, ENNReal.ofReal_toReal (measure_ne_top _ _)]
  · exact (integrable_density hκν a hs).restrict
  · exact ae_of_all _ (fun _ ↦ density_nonneg hκν _ _ _)

Похожие утверждения