[isabelle] Convergence for Extended Reals

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?


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