integrable_add_iff_of_nonpos — Mathlib

English

Let 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 < ∞.

LaTeX

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

Lean4

theorem integrable_add_iff_of_nonpos {f g : α → ℝ} (h_meas : AEStronglyMeasurable f μ) (hf : f ≤ᵐ[μ] 0)
    (hg : g ≤ᵐ[μ] 0) : Integrable (f + g) μ ↔ Integrable f μ ∧ Integrable g μ :=
  by
  rw [← integrable_neg_iff, ← integrable_neg_iff (f := f), ← integrable_neg_iff (f := g), neg_add]
  exact
    integrable_add_iff_of_nonneg h_meas.neg (hf.mono (fun _ ↦ neg_nonneg_of_nonpos))
      (hg.mono (fun _ ↦ neg_nonneg_of_nonpos))

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