Re: [isabelle] Extended non-negative reals summing to infinity

Hi Johannes,

Thanks a lot. This worked great.


On 09/07/17 23:43, Johannes HÃlzl wrote:
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.

    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,

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

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.