[isabelle] Extended non-negative reals summing to infinity



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




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