## Stream: Is there code for X?

### Topic: summable_abs_iff

#### Yury G. Kudryashov (Oct 09 2020 at 04:39):

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 (Oct 09 2020 at 04:41):

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

Last updated: May 07 2021 at 21:10 UTC