withDensity_add_measure — Mathlib

English

The density of a sum of measures equals the sum of their densities: (μ+ν).withDensity f = μ.withDensity f + ν.withDensity f.

Русский

Плотность суммы мер равна сумме плотностей: (μ+ν).withDensity f = μ.withDensity f + ν.withDensity f.

LaTeX

$$$(\mu + \nu).withDensity f = \mu.withDensity f + \nu.withDensity f$$$

Lean4

theorem withDensity_add_measure {m : MeasurableSpace α} (μ ν : Measure α) (f : α → ℝ≥0∞) :
    (μ + ν).withDensity f = μ.withDensity f + ν.withDensity f :=
  by
  ext1 s hs
  simp only [withDensity_apply f hs, restrict_add, lintegral_add_measure, Measure.add_apply]

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