withDensity_sum — Mathlib

English

For r ≥ 0, μ.withDensity (r • f) = r • μ.withDensity f.

Русский

Для r ≥ 0: μ.withDensity (r • f) = r • μ.withDensity f.

LaTeX

$$$\text{for } r \ge 0:\; \mu.withDensity (r \cdot f) = r \cdot \mu.withDensity f$$$

Lean4

theorem withDensity_sum {ι : Type*} {m : MeasurableSpace α} (μ : ι → Measure α) (f : α → ℝ≥0∞) :
    (sum μ).withDensity f = sum fun n => (μ n).withDensity f :=
  by
  ext1 s hs
  simp_rw [sum_apply _ hs, withDensity_apply f hs, restrict_sum μ hs, lintegral_sum_measure]

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