Partial sums bounded implies summable

Stream: Is there code for X?

[Kevin Buzzard]

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]

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]

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

[Sebastien Gouezel]

You have docs#not_summable_iff_tendsto_nat_at_top_of_nonneg

[Kevin Buzzard]

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

[Sebastien Gouezel]

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]

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]

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

[Sebastien Gouezel]

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

[Mario Carneiro]

Well there is has_sum if you want both at once

[Mario Carneiro]

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]

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]

I think not_summable_iff_tendsto_nat_at_top_of_nonneg should have the negation on the other side

[Sebastien Gouezel]

#5363. This should have been already in mathlib.

[Kevin Buzzard]

Thanks!

[Sebastien Gouezel]

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]

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