Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Convergence for Extended Reals


view this post on Zulip Email Gateway (Aug 22 2022 at 11:52):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear all,

I have a sequence of extended reals (f :: nat => ereal), of which I know that two
consecutive numbers differ by ever smaller amounts. In detail, I have

abs (f (Suc n) - f n) < c / 2 ^ n

for some fixed c > 0 and all n, and I'd like to prove that f converges, i.e., the limit
"lim f" exists. What is the best way to prove this?

Unfortunately, f is not monotonically increasing, so I cannot use SUP instead of lim.
On ereal, I have not found the lemma convergent_ereal, but that did not get me much
further. So I tried to do a case distinction on whether f is always a real and try to
prove "Cauchy (real o f)". but I have not found many useful lemmas about Cauchy either.
Probably I can prove everything by using metric_CauchyI, but this looks like a lot of
arithmetic on reals. Is there something more abstract?

Best,
Andreas


Last updated: Mar 29 2024 at 12:28 UTC