Zulip Chat Archive

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,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?

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).

Heather Macbeth (Jun 29 2020 at 03:31):

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

Heather Macbeth (Jun 29 2020 at 03:32):

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

Heather Macbeth (Jun 29 2020 at 03:35):

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

Kevin Buzzard (Jun 29 2020 at 09:21):

Thank you very much for these observations Heather!

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!

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.

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!