setIntegral_withDensity_eq_setIntegral_toReal_smul

English

If f is a density, then the real scalar smul interacts with the integral under a density: ∫ g d(μ.withDensity f) = ∫ (f.toReal) • g dμ.

Русский

Если f — плотность, то скалярное умножение в вещественном виде и интеграл в рамках плотности удовлетворяют формуле: ∫ g d(μ.withDensity f) = ∫ (f.toReal) • g dμ.

LaTeX

$$$\\int x in s, g x \\ d(μ.WithDensity f) = \\int x in s, f(x).toReal \\cdot g(x) \\ dμ$$$

Lean4

theorem setIntegral_withDensity_eq_setIntegral_toReal_smul {f : X → ℝ≥0∞} {s : Set X} (hf : Measurable f)
    (hf_top : ∀ᵐ x ∂μ.restrict s, f x < ∞) (g : X → E) (hs : MeasurableSet s) :
    ∫ x in s, g x ∂μ.withDensity (fun x => f x) = ∫ x in s, (f x).toReal • g x ∂μ :=
  setIntegral_withDensity_eq_setIntegral_toReal_smul₀ hf.aemeasurable hf_top g hs

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