## Stream: Is there code for X?

### Topic: Partial sums bounded implies summable

#### 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

#### 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

#### 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)

#### Kevin Buzzard (Dec 14 2020 at 09:43):

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

#### 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


#### 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?

#### Kevin Buzzard (Dec 14 2020 at 09:48):

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

#### Sebastien Gouezel (Dec 14 2020 at 09:48):

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

#### Mario Carneiro (Dec 14 2020 at 09:51):

Well there is has_sum if you want both at once

#### 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

#### 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


#### 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

#### Sebastien Gouezel (Dec 14 2020 at 10:06):

#5363. This should have been already in mathlib.

Thanks!

#### 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: $\sum_n f (k + n)$ tends to $0$ when $k$ tends to infinity, whether $f$ 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.

#### 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