English
The lintegral is additive: (f+g).lintegral μ = f.lintegral μ + g.lintegral μ for simple f,g.
Русский
Линегральный интеграл аддитивен: lintegral суммы равен сумме линегралов.
LaTeX
$$$ (f+g).lintegral\ μ = f.lintegral\ μ + g.lintegral\ μ $$$
Lean4
theorem add_lintegral (f g : α →ₛ ℝ≥0∞) : (f + g).lintegral μ = f.lintegral μ + g.lintegral μ :=
calc
(f + g).lintegral μ = ∑ x ∈ (pair f g).range, (x.1 * μ (pair f g ⁻¹' { x }) + x.2 * μ (pair f g ⁻¹' { x })) := by
rw [add_eq_map₂, map_lintegral]; exact Finset.sum_congr rfl fun a _ => add_mul _ _ _
_ = (∑ x ∈ (pair f g).range, x.1 * μ (pair f g ⁻¹' { x })) + ∑ x ∈ (pair f g).range, x.2 * μ (pair f g ⁻¹' { x }) :=
by rw [Finset.sum_add_distrib]
_ = ((pair f g).map Prod.fst).lintegral μ + ((pair f g).map Prod.snd).lintegral μ := by
rw [map_lintegral, map_lintegral]
_ = lintegral f μ + lintegral g μ := rfl
