summable vs has_sum

Stream: maths

[Filippo A. E. Nuccio]

I am playing a bit with the topology/algebra/infinite_sum file and I see that there are many results stated for the has_sum property and not for the summable one. They are equivalent, somehow, but I find myself doing

((has_sum_subtype_iff_of_support_subset this).mp (summable.has_sum _)).summable,

to get the (missing)

lemma (hf : support f ⊆ s) :  summable (f ∘ coe : s → α) a → summable f a :=

Indeed, the library has

(hf : support f ⊆ s) :
  has_sum (f ∘ coe : s → α) a ↔ has_sum f a :=

and I am going back-and-forth twice. Is there a specific reason for this choice (e.g. there is a shorter workaround) or should I add these lemma in a PR? In the first case, would it worth it to add something to the doc?

[Floris van Doorn]

Not too familiar with this part of the library, but I expect it is just missing API since summable is used less than has_sum.

[Filippo A. E. Nuccio]

Ok, I might wait for @Yury G. Kudryashov to give his advice (I think he developed most of it) and then I will open a PR.

[Eric Wieser]

I think most of the summable results can be proved with a one-liner using has_sum? What's src#summable defined as?

[Eric Wieser]

Although I guess that's basically what you have already

[Eric Wieser]

If you PR what you have above, it should be the iff version to match the one for has_sum, not the of version in your message.

[Yury G. Kudryashov]

You can use docs#exists_congr to get your theorem from has_sum version.