Email Gateway (Aug 22 2022 at 11:52): 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: Nov 21 2024 at 12:39 UTC