setIntegral_withDensity_eq_setIntegral_toReal_smul₀

English

Integrals with density on a subset equal integrals with smul by the density factor.

Русский

Интегралы по подмножеству с плотностью равны интегралам после умножения на плотность.

LaTeX

$$$\int_{s} g \; dμ = \int ( (f).toReal • g) \; dμ$$$

Lean4

theorem setIntegral_withDensity_eq_setIntegral_toReal_smul₀ {f : X → ℝ≥0∞} {s : Set X}
    (hf : AEMeasurable f (μ.restrict s)) (hf_top : ∀ᵐ x ∂μ.restrict s, f x < ∞) (g : X → E) (hs : MeasurableSet s) :
    ∫ x in s, g x ∂μ.withDensity (fun x => f x) = ∫ x in s, (f x).toReal • g x ∂μ := by
  rw [restrict_withDensity hs, integral_withDensity_eq_integral_toReal_smul₀ hf hf_top]

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