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



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






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