integrable_add_iff_of_nonneg — Mathlib

English

Let AEStronglyMeasurable f μ with f ≥ 0 a.e. and g ≥ 0 a.e. Then ∫(f+g) finite iff ∫f finite and ∫g finite.

Русский

Пусть f ≥ 0 a.e. и g ≥ 0 a.e. и f (плюс) g интегрируемы тогда ∫(f+g) < ∞ тогда и только если ∫f < ∞ и ∫g < ∞.

LaTeX

$$$ (AEStronglyMeasurable\ f\ μ) \\land (0 \\le f)\\ a.e.\ μ \\land (0 \\le g)\\ a.e.\ μ \\Rightarrow (Integrable(f+g)\\ μ \\iff (Integrable(f)\\ μ \\land Integrable(g)\\ μ)) $$$

Lean4

theorem integrable_add_iff_of_nonneg {f g : α → ℝ} (h_meas : AEStronglyMeasurable f μ) (hf : 0 ≤ᵐ[μ] f)
    (hg : 0 ≤ᵐ[μ] g) : Integrable (f + g) μ ↔ Integrable f μ ∧ Integrable g μ :=
  ⟨fun h ↦
    ⟨integrable_left_of_integrable_add_of_nonneg h_meas hf hg h,
      integrable_right_of_integrable_add_of_nonneg h_meas hf hg h⟩,
    fun ⟨hf, hg⟩ ↦ hf.add hg⟩

Похожие утверждения