setLIntegral_withDensity_eq_setLIntegral_mul

English

The same density identity holds when restricting to a measurable set s.

Русский

То же тождество плотности сохраняется при ограничении к измеримому множеству s.

LaTeX

$$∫⁻ x in s, g x d(μ.withDensity f) = ∫⁻ x in s, (f * g) x dμ$$

Lean4

theorem setLIntegral_withDensity_eq_setLIntegral_mul (μ : Measure α) {f g : α → ℝ≥0∞} (hf : Measurable f)
    (hg : Measurable g) {s : Set α} (hs : MeasurableSet s) :
    ∫⁻ x in s, g x ∂μ.withDensity f = ∫⁻ x in s, (f * g) x ∂μ := by
  rw [restrict_withDensity hs, lintegral_withDensity_eq_lintegral_mul _ hf hg]

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