summable_Lp_add — Mathlib

English

If f^p and g^p are summable, then (f+g)^p is summable as well.

Русский

Если f^p и g^p суммируемы, то и (f+g)^p суммируемо.

LaTeX

$$$\text{Summable}(f_i^p) \land \text{Summable}(g_i^p) \Rightarrow \text{Summable}((f_i+g_i)^p)$$$

Lean4

theorem summable_Lp_add {f g : ι → ℝ≥0} {p : ℝ} (hp : 1 ≤ p) (hf : Summable fun i => f i ^ p)
    (hg : Summable fun i => g i ^ p) : Summable fun i => (f i + g i) ^ p :=
  (Lp_add_le_tsum hp hf hg).1

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