English
Let f,g: α → ℝ≥0∞ with f measurable. Then the lintegral of f+g equals the sum of lintegrals: ∫⁻ (f+g) dμ = ∫⁻ f dμ + ∫⁻ g dμ.
Русский
Пусть f,g: α → ℝ≥0∞ и f измерима. Тогда линеграл от f+g равен сумме линегралов: ∫⁻ (f+g) dμ = ∫⁻ f dμ + ∫⁻ g dμ.
LaTeX
$$$\forall f,g : \alpha \to \mathbb{R}_{\ge 0}^{\infty},\; \mathrm{Measurable}(f) \Rightarrow \int^- a, f a + g a \partial\mu = \int^- a, f a \partial\mu + \int^- a, g a \partial\mu$$$
Lean4
/-- If `f g : α → ℝ≥0∞` are two functions and one of them is (a.e.) measurable, then the Lebesgue
integral of `f + g` equals the sum of integrals. This lemma assumes that `f` is integrable, see also
`MeasureTheory.lintegral_add_right` and primed versions of these lemmas. -/
@[simp]
theorem lintegral_add_left {f : α → ℝ≥0∞} (hf : Measurable f) (g : α → ℝ≥0∞) :
∫⁻ a, f a + g a ∂μ = ∫⁻ a, f a ∂μ + ∫⁻ a, g a ∂μ :=
by
refine le_antisymm ?_ (le_lintegral_add _ _)
rcases exists_measurable_le_lintegral_eq μ fun a => f a + g a with ⟨φ, hφm, hφ_le, hφ_eq⟩
calc
∫⁻ a, f a + g a ∂μ = ∫⁻ a, φ a ∂μ := hφ_eq
_ ≤ ∫⁻ a, f a + (φ a - f a) ∂μ := (lintegral_mono fun a => le_add_tsub)
_ = ∫⁻ a, f a ∂μ + ∫⁻ a, φ a - f a ∂μ := (lintegral_add_aux hf (hφm.sub hf))
_ ≤ ∫⁻ a, f a ∂μ + ∫⁻ a, g a ∂μ := add_le_add_left (lintegral_mono fun a => tsub_le_iff_left.2 <| hφ_le a) _
