integral_withDensity_eq_integral_toReal_smul₀

English

For f: X → ℝ≥0 and a measurable set s, Integrable on restricted μ.restrict s, ∫ g d(μ.withDensity f).restrict s = ∫ f·g dμ on s.

Русский

Для f: X → ℝ≥0 и множества s; если g интегрируем на ограниченной мере μ.restrict s, то соответствующая равенство для density держится на s.

LaTeX

$$$\\int_X g(x) \\,d(\\mu.withDensity f) = \\int_X f(x)\\,g(x) \\,d\\mu$ (на ограничении по s)$$

Lean4

theorem integral_withDensity_eq_integral_toReal_smul₀ {f : X → ℝ≥0∞} (f_meas : AEMeasurable f μ)
    (hf_lt_top : ∀ᵐ x ∂μ, f x < ∞) (g : X → E) : ∫ x, g x ∂μ.withDensity f = ∫ x, (f x).toReal • g x ∂μ :=
  by
  dsimp only [ENNReal.toReal, ← NNReal.smul_def]
  rw [← integral_withDensity_eq_integral_smul₀ f_meas.ennreal_toNNReal,
    withDensity_congr_ae (coe_toNNReal_ae_eq hf_lt_top)]

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