real.summable_of_sum_le

Stream: Is there code for X?

[Adam Topaz]

I'm sure we have something along these lines, but I can't seem to find anything...

import analysis.normed_space.basic

variables {α : Type*} (f : α → ℝ)

open_locale big_operators

lemma summable_of_finset_sum_le (c : ℝ) (hf : ∀ a, 0 ≤ f a)
  (cond : ∀ (S : finset α), ∑ a in S, f a ≤ c) : summable f := sorry

[Heather Macbeth]

There is a sort of mechanism to do this thing, see @Gihan Marasingha's proof of Bessel's inequality: docs#orthonormal.inner_products_summable

[Heather Macbeth]

You would say

use Sup (set.range (λ S : finset α, ∑ a in S, f a))

to provide a candidate for the sum, and then

apply has_sum_of_is_lub_of_nonneg,

to get goals which cond allows you to prove.

[Heather Macbeth]

I wrote docs#has_sum_of_is_lub_of_nonneg. If I remember correctly, the reason I didn't at the time provide a corollary along the lines you mention is that I thought it should apply to complete linear ordered add_monoids, or something like that, and there was no way of stating this kind of typeclass condition because of the algebraic order properties not being mixins. Maybe @Damiano Testa's refactor has since fixed this!

[Adam Topaz]

Thanks @Heather Macbeth ! I think for now I can get by with has_sum_of_is_lub_of_nonneg.

[Anatole Dedecker]

I did prove this a few days ago, it should be docs#summable_of_sum_le