setIntegral_withDensity_eq_setIntegral_toReal_smul₀'

English

Let μ be a finite measure on X, s ⊆ X, f: X → ℝ≥0∞ with hf AEMeasurable on μ.restrict s and hf_top: ∀ᵐ x ∂μ.restrict s, f x < ∞, and g: X → E. Then ∫_{x∈s} g(x) dμ.withDensity f = ∫_{x∈s} (f(x)).toReal · g(x) dμ.

Русский

Пусть μ—конечная мера на X, s ⊆ X, f: X → ℝ≥0∞ с hf AEMeasurable на μ.restrict s и hf_top: почти наверняка f(x) < ∞ на μ.restrict s, и g: X → E. Тогда ∫_{x∈s} g(x) dμ.withDensity f = ∫_{x∈s} f(x).toReal · g(x) dμ.

LaTeX

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

Lean4

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

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