*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>, isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Extended non-negative reals summing to infinity*From*: Johannes Hölzl <johannes.hoelzl at gmx.de>*Date*: Sun, 09 Jul 2017 22:43:34 +0100*In-reply-to*: <0d9af6ed-3117-9963-e583-29f9e4928039@inf.ethz.ch>*References*: <0d9af6ed-3117-9963-e583-29f9e4928039@inf.ethz.ch>

Am Freitag, den 07.07.2017, 15:25 +0200 schrieb Andreas Lochbihler: > Dear list, > > I'm trying to prove that it I have a diverging summation expressed > using "nn_integralÂ > (count_space UNIV)", then there is a finite prefix that is larger > than a given bound.Â > Formally: > > lemma > ÂÂÂfixes f :: "nat => ennreal" and b :: ennreal > ÂÂÂassumes "nn_integral (count_space UNIV) f = top" > ÂÂÂand "b < top" > ÂÂÂobtains n where "b < sum f {..n}" > > What's the best way to prove this? > > Thanks a lot, > Andreas > I guess nn_integral_count_space_nat is a good theorem. Then (SUP n.Âsum f {..n}) = (âi. f i) = top suminf_eq_SUP and SUP_eq_top_iff prove the statement. - Johannes

**Follow-Ups**:**Re: [isabelle] Extended non-negative reals summing to infinity***From:*Andreas Lochbihler

**References**:**[isabelle] Extended non-negative reals summing to infinity***From:*Andreas Lochbihler

- Previous by Date: [isabelle] Concept of a small logical kernel, preserving logical dependencies, axiomatic type classes vs. type abstraction, Isabelle documentation â Re: Verify the legitimacy of a proof?
- Next by Date: [isabelle] Code equations get eta-contracted
- Previous by Thread: [isabelle] Extended non-negative reals summing to infinity
- Next by Thread: Re: [isabelle] Extended non-negative reals summing to infinity
- Cl-isabelle-users July 2017 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list