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