Zulip Chat Archive

Stream: Is there code for X?

Topic: transcendence of pi


view this post on Zulip Kevin Buzzard (Jun 28 2020 at 00:26):

I have a student working on transcendence of pi in Lean. Does mathlib yet have a proof that if F is some polynomial in x,ex,sin(x),cos(x)x,e^x,\sin(x),\cos(x) with real coefficients, and deriv F is its derivative, then the integral of deriv F from a to b is F b - F a?

view this post on Zulip Heather Macbeth (Jun 29 2020 at 03:28):

I have never read the proof of Lindemann-Weierstrass, but judging from the Wikipedia article, what he or she needs is some inequalities in the elementary functions. Indeed, if the standard proof of such an inequality uses the fundamental theorem of calculus (not in mathlib), it should be perfectly possible to translate it to a proof using the Lagrange remainder formula for Taylor's theorem (a quick corollary of the Mean Value Theorem, which is in mathlib).

view this post on Zulip Heather Macbeth (Jun 29 2020 at 03:31):

For example, consider the proof of Lemma A. The required inequality is that if f(s)f(s) is a polynomial of degree dd, and I(s)=esj=0df(j)(0)j=0df(j)(s)I(s)=e^s\sum_{j=0}^df^{(j)}(0)-\sum_{j=0}^df^{(j)}(s), then, lettting F(s)F(s) be the polynomial whose coefficients are the absolute values of those of f(s)f(s), we have, I(s)sesF(s)|I(s)|\leq |s|e^{|s|}F(|s|).

view this post on Zulip Heather Macbeth (Jun 29 2020 at 03:32):

By triangle inequality it should suffice to prove this for a monomial, f(s)=sdf(s)=s^d.

view this post on Zulip Heather Macbeth (Jun 29 2020 at 03:35):

And then if I calculate correctly, the quantity I(s)I(s) becomes d![esi=0d1i!si]d!\left[e^s-\sum_{i=0}^d\frac{1}{i!}s^i\right], which is the discrepancy between ese^s and its dd-th Taylor polynomial; then the Lagrange remainder formula gives the estimate required.

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 09:21):

Thank you very much for these observations Heather!

view this post on Zulip Sebastien Gouezel (Jun 29 2020 at 09:29):

I should mention a nice formalization in Isabelle: https://www.isa-afp.org/entries/Pi_Transcendental.html. It should be possible to follow it essentially step by step in Lean!

view this post on Zulip Johan Commelin (Jun 29 2020 at 09:36):

If we are making comments about this proof, let me add that Lindemann cooked up this proof while hiking through the Black Forest near Freiburg! We have a bust of him in our department.

view this post on Zulip Kevin Buzzard (Jul 01 2020 at 16:55):

I should say now that the student is @Jujian Zhang and he has warmed up by proving transcendence of e! He needed FTC and a couple of corollaries like integration by parts, but other than a few axioms the proof compiles!

view this post on Zulip Johan Commelin (Jul 01 2020 at 17:05):

Congratulations!


Last updated: May 17 2021 at 15:13 UTC