Retrieving a Cauchy Sequence from a Real?

Stream: new members

[Andrew Elsey]

So essentially, let's say I have any real value, r. I can call r.cauchy to get a member of a quotient (called Cauchy). I would like to get the (or, more acurrately, a/an) underlying rational sequence. I'm wondering if this is possible. Is there any way to retrieve any representative member of the fiber of the Cauchy value (I believe a term of type cau_seq)? I guess this is a question about quotients in general.

[Eric Rodriguez]

x.cauchy.out

[Eric Rodriguez]

there may be a more API-ful way

[Andrew Elsey]

Eric Rodriguez said:

there may be a more API-ful way

Thanks. Ah, I guess getting a computable sequence was be a pipe dream lol

[Eric Rodriguez]

what sort of computable sequence are you hoping to get for, say, Chaitin's constant? :b

[Andrew Elsey]

Eric Rodriguez said:

what sort of computable sequence are you hoping to get for, say, Chaitin's constant? :b

Point taken. My aims were a lot less grand. Compute angles from rational vectors using the appropriate lean instances and convert sets of angles into rational bases. Can't have my pi and approximate it too :(

[Andrew Elsey]

(deleted)

[Eric Rodriguez]

I'm sure for pi there'll be a series definition somewhere!

[Eric Rodriguez]

docs#real.tendsto_prod_pi_div_two seems to establish the Wallis product

[Eric Rodriguez]

and Leibniz's series is somewhere slightly higher up the file

[Eric Wieser]

Note that if you use docs#quotient.lift you can still compute functions of a particular sequence as long as you show that the result doesn't depend on which sequence you used