setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable

English

For a measurable set s and a density f having suitable almost everywhere finiteness, the restricted lintegral over s with density f equals the restricted lintegral over s of f·g w.r.t μ.

Русский

Для измеримого множества s и плотности f c условий, ограниченный линтеграл по s от g с плотностью f равен ограниченному линтегралу по s от f·g относительно μ.

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∞}
    (f_meas : Measurable f) (g : α → ℝ≥0∞) {s : Set α} (hs : MeasurableSet s) (hf : ∀ᵐ 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 _ f_meas hf]

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