Bounds on Pi with arbitrary precision

Stream: maths

[Tomaz Gomes]

Since the definition of Real.pi is marked as noncomputable, I can't ask Lean's kernel to check if a given number is smaller than pi, right? So, in order to obtain a proof that my number is smaller than pi, I would use pi_gt_3141592 together with lt_trans. But with this I can only prove that numbers up to 3.141592 are smaller than pi. Is there a method for checking it for numbers arbitrarily close to pi? Maybe using tendsto_sum_pi_div_four?

[Kevin Buzzard]

Do you mean "a method" or "something which actually works in practice"?

[Tomaz Gomes]

I mean "something which actually works in practice", could be a tactic

[Eric Wieser]

Did you look at the tactic next to that lemma?

[Kevin Buzzard]

The thing about docs#Real.tendsto_sum_pi_div_four is that it will take a very long time to beat 3.141592

[Kevin Buzzard]

There are much better ways to approximate $\pi$.

[Tomaz Gomes]

Eric Wieser said:

Did you look at the tactic next to that lemma?

Yes, maybe I could use it to obtain a bound tighter than 3.141592, but I don't see a way to generalize it so I can obtain arbitrary precision

[Kevin Buzzard]

This lemma is giving you arbitrary precision

[Eric Wieser]

I assume you mean tactic, Kevin?

[Tomaz Gomes]

Kevin Buzzard said:

This lemma is giving you arbitrary precision

Yes, but in order to obtain a bound I have to provide a complicated sequence of numbers. So, for instance, to write a tactic that could, for any number x lesser than pi, produce a proof for x < Real.pi I would have to come up with an algorithm that generates a sequence with the property required by that tactic, which seems hard to me (maybe it is not, I am not an expert on this)

[Kevin Buzzard]

That doesn't look too hard to me. You can just recursively make that sequence. Did you try working out an example already in mathlib?

[Tomaz Gomes]

No... okay, I will try then, thanks!

[Kevin Buzzard]

It seems to me that the trick is something like this. You have to make a sequence of numbers $r_1,r_2,\ldots,r_n$ and the sequence is increasing and starts off bigger than $\sqrt{2}$ and is forced to go up at a certain rate. This means $\sqrt{2-r_n}$ is going down, and you need to make it go down as slowly as possible because you want $a/2^{n+1}$ to overtake it ASAP. So you make rational approximations to the actual square root values bounding the $r_i$ which are as tight as possible whilst not going too crazy with denominators (use partial fractions, for example).

[Kevin Buzzard]

For example the first rational numbers which appear in the mysterious-looking sequences in the proofs are just slightly bigger than $\sqrt{2}$, and the second ones are all very close to $\sqrt{2+\sqrt2}$