English
Let μ be a finite measure on X, s a measurable subset of X, f: X → ℝ≥0 with f AEMeasurable on μ.restrict s, and g: X → E. Then the Bochner integral of g over s with respect to μ.withDensity (f) equals the Bochner integral of f(x) · g(x) with respect to μ, i.e. ∫_{x∈s} g(x) dμ.withDensity(f) = ∫_{x∈s} f(x) · g(x) dμ.
Русский
Пусть μ—кратная мера на X, s — измеримая подмножество X, f: X → ℝ≥0, AEMeasurable на μ.restrict s, и g: X → E. Тогда интеграл Боунхер по x на s относительно μ с плотностью f равен интегралу по μ от f(x) · g(x): ∫_{x∈s} g(x) dμ.withDensity(f) = ∫_{x∈s} f(x) · g(x) dμ.
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₀' [SFinite μ] {f : X → ℝ≥0} (s : Set X)
(hf : AEMeasurable f (μ.restrict s)) (g : X → E) :
∫ x in s, g x ∂μ.withDensity (fun x => f x) = ∫ x in s, f x • g x ∂μ := by
rw [restrict_withDensity' s, integral_withDensity_eq_integral_smul₀ hf]
