Zulip Chat Archive

Stream: Is there code for X?

Topic: Partial sums bounded implies summable


view this post on Zulip Kevin Buzzard (Dec 14 2020 at 09:18):

I have an infinite sequence of non-negative reals and I can prove that all finite sums (ie sum of the first M terms, although I could extend this to any finset without much trouble) are <= c. Is there a relatively painless way to prove that the infinite sum is summable and also <= c? I could just plough through the first principles proof but I'm hoping there's already something useful there. This is for the Scholze challenge, in case anyone is wondering why I'm doing analysis

view this post on Zulip Mario Carneiro (Dec 14 2020 at 09:27):

The existing theorems look a little disappointing for this use case. I see two easiest paths: (1) transfer to ennreal, where sums are nice, and use your proof to show that it is <= c and thus finite, and transfer back. (2) Use bolzano-weierstrass on [0, c] as a compact set in R

view this post on Zulip Mario Carneiro (Dec 14 2020 at 09:28):

(Note that proving the sum is <= c is the easy part; the hard part is proving summable f)

view this post on Zulip Sebastien Gouezel (Dec 14 2020 at 09:35):

You have docs#not_summable_iff_tendsto_nat_at_top_of_nonneg

view this post on Zulip Kevin Buzzard (Dec 14 2020 at 09:43):

Thanks Sebastien -- perhaps this is the most painless route.

view this post on Zulip Sebastien Gouezel (Dec 14 2020 at 09:45):

lemma summable_of_sum_range_le {f :   } {c : } (hf :  n, 0  f n)
  (h :  n,  i in finset.range n, f i  c) : summable f :=
begin
  by_contra H,
  rcases exists_lt_of_tendsto_at_top ((not_summable_iff_tendsto_nat_at_top_of_nonneg hf).1 H) 0 c
    with n, -, hn⟩,
  exact lt_irrefl _ (hn.trans_le (h n)),
end

view this post on Zulip Johan Commelin (Dec 14 2020 at 09:46):

Is it possible to design tsum in such a way that we don't have to prove summable f and summable g as side conditions for almost every lemma out there?

view this post on Zulip Kevin Buzzard (Dec 14 2020 at 09:48):

But they are necessary conditions for almost every proof out there!

view this post on Zulip Sebastien Gouezel (Dec 14 2020 at 09:48):

Normally all lemmas where the summability is not necessary should be stated without the summability assumption.

view this post on Zulip Mario Carneiro (Dec 14 2020 at 09:51):

Well there is has_sum if you want both at once

view this post on Zulip Mario Carneiro (Dec 14 2020 at 09:52):

I think tsum only has an advantage on things like ennreal where summable is trivial for a reason unrelated to the function itself

view this post on Zulip Sebastien Gouezel (Dec 14 2020 at 09:52):

lemma tsum_le_of_sum_range_le {f :   } {c : } (hf :  n, 0  f n)
  (h :  n,  i in finset.range n, f i  c) : (∑' n, f n)  c :=
le_of_tendsto' ((has_sum_iff_tendsto_nat_of_nonneg hf _).1 (summable_of_sum_range_le hf h).has_sum) h

view this post on Zulip Mario Carneiro (Dec 14 2020 at 09:53):

I think not_summable_iff_tendsto_nat_at_top_of_nonneg should have the negation on the other side

view this post on Zulip Sebastien Gouezel (Dec 14 2020 at 10:06):

#5363. This should have been already in mathlib.

view this post on Zulip Kevin Buzzard (Dec 14 2020 at 10:13):

Thanks!

view this post on Zulip Sebastien Gouezel (Dec 14 2020 at 11:03):

Johan Commelin said:

Is it possible to design tsum in such a way that we don't have to prove summable f and summable g as side conditions for almost every lemma out there?

In fact while browsing the file I noticed a lemma where the summability assumption is not necessary: nf(k+n)\sum_n f (k + n) tends to 00 when kk tends to infinity, whether ff is summable or not (because in the latter situation all sums are zero :-). Fixed (is that the right word, or should I use obfuscated?) in #5366.

view this post on Zulip Johan Commelin (Dec 14 2020 at 11:10):

Thanks! That will simplify the proof that I worked on Saturday


Last updated: May 07 2021 at 19:12 UTC