setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀'

English

A variant with SFinite measures asserts the same restricted density equality under assumptions on a.e. finiteness and measurability on s.

Русский

Вариант с SFinite мерам устанавливает то же самое равенство плотности на ограниченном множестве при предположениях относительно a.e. конечности и измеримости на 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 α) [SFinite μ] {f : α → ℝ≥0∞}
    (s : Set α) (hf : AEMeasurable f (μ.restrict s)) (g : α → ℝ≥0∞) (h'f : ∀ᵐ x ∂μ.restrict s, f x < ∞) :
    ∫⁻ a in s, g a ∂μ.withDensity f = ∫⁻ a in s, (f * g) a ∂μ := by
  rw [restrict_withDensity' s, lintegral_withDensity_eq_lintegral_mul_non_measurable₀ _ hf h'f]

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