integral_withDensity_eq_integral_toReal_smul

English

For f: X → ℝ≥0∞, measurable and integrability y, ∫ g d(μ.withDensity f) = ∫ (f x).toReal • g x dμ.

Русский

Для плотности f: X → ℝ≥0∞ интегрируемое g: X → E, имеем равенство через toReal плотности.

LaTeX

$$$\\int_X g(x) \\,d(\\mu.withDensity f) = \\int_X (f(x)).toReal \\;\\cdot g(x) \\,d\\mu$$$

Lean4

theorem integral_withDensity_eq_integral_toReal_smul {f : X → ℝ≥0∞} (f_meas : Measurable f)
    (hf_lt_top : ∀ᵐ x ∂μ, f x < ∞) (g : X → E) : ∫ x, g x ∂μ.withDensity f = ∫ x, (f x).toReal • g x ∂μ :=
  integral_withDensity_eq_integral_toReal_smul₀ f_meas.aemeasurable hf_lt_top g

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