setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀

English

Given f,a.e. measurable and g, for any set s, the restricted lintegral equality holds under appropriate almost-everywhere finiteness.

Русский

Пусть f a.e. измеримо и g; для любого множества s справедливо равенство ограниченного линтеграла при надлежащем условии конечности почти везде.

LaTeX

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

Lean4

theorem setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀ (μ : Measure α) {f : α → ℝ≥0∞} {s : Set α}
    (hf : AEMeasurable f (μ.restrict s)) (g : α → ℝ≥0∞) (hs : MeasurableSet s) (h'f : ∀ᵐ x ∂μ.restrict s, f x < ∞) :
    ∫⁻ a in s, g a ∂μ.withDensity f = ∫⁻ a in s, (f * g) a ∂μ := by
  rw [restrict_withDensity hs, lintegral_withDensity_eq_lintegral_mul_non_measurable₀ _ hf h'f]

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