Zulip Chat Archive

Stream: Is there code for X?

Topic: summable_abs_iff


view this post on Zulip 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∥)?

view this post on Zulip 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