integral_density — Mathlib

English

The lintegral of density equals the real-valued kernel measure on univ.

Русский

Линеграль интеграл плотности равен реальным значениям меры ядра на универсума.

LaTeX

$$lintegral (coeff ν a) (fun x => density ν a x s) = (κ a).real (univ ×ˢ s)$$

Lean4

theorem integral_density (hκν : fst κ ≤ ν) [IsFiniteKernel ν] (a : α) {s : Set β} (hs : MeasurableSet s) :
    ∫ x, density κ ν a x s ∂(ν a) = (κ a).real (univ ×ˢ s) := by
  rw [← setIntegral_univ, setIntegral_density_of_measurableSet hκν 0 a hs MeasurableSet.univ]

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