Stream: Archive Mirror: Isabelle Users Mailing List

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

Email Gateway (Aug 22 2022 at 15:40):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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

Email Gateway (Aug 22 2022 at 15:44):

From: Johannes Hölzl <johannes.hoelzl@gmx.de>
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

Email Gateway (Aug 22 2022 at 15:45):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Johannes,

Thanks a lot. This worked great.

Andreas

Last updated: Nov 21 2024 at 12:39 UTC