withDensity_add_left — Mathlib

English

If f is measurable, then μ.withDensity (f+g) = μ.withDensity f + μ.withDensity g.

Русский

Если f измерима, то μ.withDensity (f+g) = μ.withDensity f + μ.withDensity g.

LaTeX

$$$f\,\text{measurable} \Rightarrow \mu.withDensity (f+g) = \mu.withDensity f + \mu.withDensity g$$$

Lean4

theorem withDensity_add_left {f : α → ℝ≥0∞} (hf : Measurable f) (g : α → ℝ≥0∞) :
    μ.withDensity (f + g) = μ.withDensity f + μ.withDensity g :=
  by
  refine Measure.ext fun s hs => ?_
  rw [withDensity_apply _ hs, Measure.add_apply, withDensity_apply _ hs, withDensity_apply _ hs, ←
    lintegral_add_left hf]
  simp only [Pi.add_apply]

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