setLIntegral_withDensity_eq_lintegral_mul₀

English

For any measurable set s, f,a.e.measurable, g a.e. measurable, the restricted lintegral over s with density f equals the restricted lintegral of f·g over s with respect to μ.

Русский

Для любого измеримого множества s, f a.e. измеримо, g a.e. измеримо: линтеграл по 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_lintegral_mul₀ {μ : Measure α} {f : α → ℝ≥0∞} (hf : AEMeasurable f μ) {g : α → ℝ≥0∞}
    (hg : AEMeasurable g μ) {s : Set α} (hs : MeasurableSet s) :
    ∫⁻ a in s, g a ∂μ.withDensity f = ∫⁻ a in s, (f * g) a ∂μ :=
  setLIntegral_withDensity_eq_lintegral_mul₀' hf (hg.mono' (MeasureTheory.withDensity_absolutelyContinuous μ f)) hs

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