setIntegral_withDensity_eq_setIntegral_smul₀

English

For f: X → ℝ≥0 and s measurable, for all g: X → E, ∫ x in s g x d(μ.withDensity f) = ∫ x in s f x • g x dμ.

Русский

Для плотности f на измеримом множестве s верно: интеграл по s от g равен интегралу по плотности f на s умноженной на g.

LaTeX

$$$\\int_{x\\in s} g(x) \\,d(\\mu.withDensity f) = \\int_{x\\in s} f(x) \\cdot g(x) \\,d\\mu$$$

Lean4

theorem setIntegral_withDensity_eq_setIntegral_smul₀ {f : X → ℝ≥0} {s : Set X} (hf : AEMeasurable f (μ.restrict s))
    (g : X → E) (hs : MeasurableSet s) : ∫ x in s, g x ∂μ.withDensity (fun x => f x) = ∫ x in s, f x • g x ∂μ := by
  rw [restrict_withDensity hs, integral_withDensity_eq_integral_smul₀ hf]

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