summable_abs_iff

Stream: Is there code for X?

[Yury G. Kudryashov]

Do we have a proof of summable (f : α → ℝ) → summable (λ x, abs (f x))? I have this (depends on a few additional trivial lemmas):

lemma real.summable_abs_iff {f : ι → ℝ} : summable (λ x, abs (f x)) ↔ summable f :=
have h1 : ∀ x : {x | 0 ≤ f x}, abs (f x) = f x := λ x, abs_of_nonneg x.2,
have h2 : ∀ x : {x | 0 ≤ f x}ᶜ, abs (f x) = -f x := λ x, abs_of_neg (not_le.1 x.2),
calc summable (λ x, abs (f x)) ↔
  summable (λ x : {x | 0 ≤ f x}, abs (f x)) ∧ summable (λ x : {x | 0 ≤ f x}ᶜ, abs (f x)) :
  summable_subtype_and_compl.symm
... ↔ summable (λ x : {x | 0 ≤ f x}, f x) ∧ summable (λ x : {x | 0 ≤ f x}ᶜ, -f x) :
  by simp only [h1, h2]
... ↔ _ : by simp only [summable_neg_iff, summable_subtype_and_compl]

@Patrick Massot What is the correct generality for summable (f : α → E) → summable (λ x, ∥f x∥)?

[Yury G. Kudryashov]

For [finite_dimensional ℝ E] it easily follows from real.summable_abs_iff.