English
The sum of the lower Lebesgue integrals of two nonnegative functions does not exceed the integral of their pointwise sum.
Русский
Сумма неотрицательных интегралов не превосходит интеграл от суммы функций.
LaTeX
$$$$ \\int^{\\!-} f + \\int^{\\!-} g \\le \\int^{\\!-} (f+g). $$$$
Lean4
/-- The sum of the lower Lebesgue integrals of two functions is less than or equal to the integral
of their sum. The other inequality needs one of these functions to be (a.e.-)measurable. -/
theorem le_lintegral_add (f g : α → ℝ≥0∞) : ∫⁻ a, f a ∂μ + ∫⁻ a, g a ∂μ ≤ ∫⁻ a, f a + g a ∂μ :=
by
simp only [lintegral]
refine
ENNReal.biSup_add_biSup_le' (p := fun h : α →ₛ ℝ≥0∞ => h ≤ f) (q := fun h : α →ₛ ℝ≥0∞ => h ≤ g) ⟨0, zero_le f⟩
⟨0, zero_le g⟩ fun f' hf' g' hg' => ?_
exact le_iSup₂_of_le (f' + g') (add_le_add hf' hg') (add_lintegral _ _).ge
