Zulip Chat Archive

Stream: maths

Topic: summable vs has_sum


Filippo A. E. Nuccio (Dec 03 2021 at 15:36):

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 (Dec 03 2021 at 15:51):

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 (Dec 03 2021 at 15:52):

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 (Dec 03 2021 at 19:23):

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 (Dec 03 2021 at 19:25):

Although I guess that's basically what you have already

Eric Wieser (Dec 03 2021 at 19:27):

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 (Dec 03 2021 at 21:07):

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


Last updated: Dec 20 2023 at 11:08 UTC