Subsequence of cauchy seq

Stream: Is there code for X?

[Deniz Aydin]

Do we have that subsequences of a cauchy sequence are themselves cauchy, and equiv to the original sequence? There's stuff about subsequences in docs#cauchy, but that file seems to be about a more general idea of cauchy that I can't understand at my level, and I don't know if it shows anything relevant relevant to the docs#cau_seq defined in data.real which is what I'm interested in.

[Heather Macbeth]

@Deniz Aydin Can you say a little more about what you want this for? There might be a more high-powered way of doing your application that you wouldn't have to fight the library for.

[Anatole Dedecker]

By equiv do you mean docs#asymptotics.is_equivalent ? If so, then I don't think your lemma exists. If you really need it I can work on that tomorrow.

[Anatole Dedecker]

Also, the right notion of Cauchy sequence is almost surely docs#cauchy_seq.

[Anatole Dedecker]

And if you want to go back to the usual definition on a metric space, the right lemma is docs#metric.cauchy_seq_iff

[Deniz Aydin]

Heather's probably right that I don't need this lemma, it just seemed like the obvious way for me to show that a certain sequence is cauchy but I'm sure I can do it directly. Regardless I should have been clearer, by cauchy and equiv I do in fact mean the docs#cau_seq.equiv definition in data.real, which is the only one I knew existed until I started searching for this lemma. As far as I can tell the version you're linking is totally independent of this one which I find strange but I'm sure there's a reason.
If you're curious why I care about this version, I'm working with base b expansions of real numbers building on one of @Kevin Buzzard's experiments, and from a sequence of digits I get a real number using the cauchy sequence of summing up just the first n digits of the number. I've almost shown that this is the inverse of the map he defined here.

[Anatole Dedecker]

Yeah I just realized that asymptotic equivalence is not what you meant because it makes the statement trivially false :face_palm:

[Anatole Dedecker]

docs#cau_seq is a low level tool used to build the real numbers, and in a prefect world you shouldn't have to use it at all after proving everything you need about reals. docs#cauchy_seq is a much more general (and a bit more obscure at first) version of this which is better suited for abstract results.

[Anatole Dedecker]

In your case, it may be easier to use either :

• docs#cauchy_seq + docs#cauchy_seq_tendsto_of_is_complete to get the limit
• docs#tsum

[Deniz Aydin]

I liked the idea of using docs#cau_seq because it feels like the natural way to get a real number from a sequence af rational numbers was to go straight through the definition, that way I wouldn't have to cast rationals to reals though it probably doesn't make much difference in practice. Thanks for the advice, I may try express things in terms of tsum at some point though I'll have to do a lot of lemma hunting.