setIntegral_withDensity_eq_setIntegral_toReal_smul'

English

Under the same finite measure setting, and with f measurable on s and almost everywhere finite on μ.restrict s, the equality ∫ x∈s g x dμ.withDensity f = ∫ x∈s f(x).toReal · g x dμ holds for any g: X → E.

Русский

При той же постановке с конечной мерой и когда f измерима на s, а f конечна почти всюду относительно μ|s, выполняется тождество ∫_{x∈s} g(x) dμ^{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 : Measurable f)
    (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 ∂μ :=
  setIntegral_withDensity_eq_setIntegral_toReal_smul₀' s hf.aemeasurable hf_top g

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