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]