## Stream: new members

### Topic: Retrieving a Cauchy Sequence from a Real?

#### Andrew Elsey (Jun 26 2021 at 13:44):

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 (Jun 26 2021 at 13:55):

x.cauchy.out

#### Eric Rodriguez (Jun 26 2021 at 13:56):

there may be a more API-ful way

#### Andrew Elsey (Jun 26 2021 at 15:12):

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 (Jun 26 2021 at 15:16):

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

#### Andrew Elsey (Jun 26 2021 at 15:34):

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 :(

(deleted)

#### Eric Rodriguez (Jun 26 2021 at 16:03):

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

#### Eric Rodriguez (Jun 26 2021 at 16:07):

docs#real.tendsto_prod_pi_div_two seems to establish the Wallis product

#### Eric Rodriguez (Jun 26 2021 at 16:07):

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

#### Eric Wieser (Jun 26 2021 at 20:20):

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

Last updated: Dec 20 2023 at 11:08 UTC