∀ {ι : Type u} {f g : ι → ℝ} {p : ℝ},
  1 ≤ p →
    (∀ (i : ι), 0 ≤ f i) →
      (∀ (i : ι), 0 ≤ g i) →
        (Summable fun i => f i ^ p) → (Summable fun i => g i ^ p) → Summable fun i => (f i + g i) ^ p