English
For f and a family of measures μ_i, the lintegral equals the sum over i of the lintegrals: f.lintegral(Measure.sum μ) = ∑' i, f.lintegral(μ_i).
Русский
Для f и семейства мер μ_i линеграль равен сумме по i: f.lintegral(Measure.sum μ) = ∑' i, f.lintegral(μ_i).
LaTeX
$$$f.lintegral\\left(\\text{Measure.sum } μ\\right) = \\sum_{i}^{\\prime} f.lintegral(μ_i)$$$
Lean4
theorem lintegral_sum {m : MeasurableSpace α} {ι} (f : α →ₛ ℝ≥0∞) (μ : ι → Measure α) :
f.lintegral (Measure.sum μ) = ∑' i, f.lintegral (μ i) :=
by
simp only [lintegral, Measure.sum_apply, f.measurableSet_preimage, ← Finset.tsum_subtype, ← ENNReal.tsum_mul_left]
apply ENNReal.tsum_comm