English
The density of a pointwise sum of densities equals the sum of the corresponding density measures: μ.withDensity(∑ f_n) = ∑ μ.withDensity(f_n).
Русский
Плотность от точечной суммы плотностей равна сумме соответствующих плотностей мер: μ.withDensity(∑ f_n) = ∑ μ.withDensity(f_n).
LaTeX
$$$\\mu.withDensity\\left(\\sum\\_n f_n\\right) = \\sum\\_n \\mu.withDensity(f_n)$$$
Lean4
theorem withDensity_tsum {ι : Type*} [Countable ι] {f : ι → α → ℝ≥0∞} (h : ∀ i, Measurable (f i)) :
μ.withDensity (∑' n, f n) = sum fun n => μ.withDensity (f n) :=
by
ext1 s hs
simp_rw [sum_apply _ hs, withDensity_apply _ hs]
change ∫⁻ x in s, (∑' n, f n) x ∂μ = ∑' i, ∫⁻ x, f i x ∂μ.restrict s
rw [← lintegral_tsum fun i => (h i).aemeasurable]
exact lintegral_congr fun x => tsum_apply (Pi.summable.2 fun _ => ENNReal.summable)
