Exercices on polynomials

• Formalisation of the algebraic part of a simple proof that PI is irrational described in:
• http://projecteuclid.org/download/pdf_1/euclid.bams/1183510788

Parameters definitions:

• Let n na nb be natural numbers
• Suppose nb is a non zero nat: nb != 0
• Define the corresponding rationals a , b
• Define pi as a/b.

Definition of the polynomials:

• Look at the f definition: the factorial, the coercion nat :> R (as a Ring), etc...
• Define F:{poly rat} using bigop.

Prove that:

• b is non zero rational.

Prove that:

• (a - bX) has a size of 2

Prove that:

• the lead_coef of (a - bX) is -b.

Prove that:

• the size of (a-X)^n is n.+1

Prove that:

• Exponent and composition of polynomials combine:

Prove that:

• f's small coefficients are zero

Prove that:

• f/n! as integral coefficients

Prove that:

the f^`(i) (x) have integral values for x = 0

Deduce that:

F (0) has an integral value

Then prove

• the symmetry argument f(x) = f(pi -x).

Prove

• the symmetry for the derivative

Deduce that

• F(pi) is an integer

if you have time

• you can prove the equality F^`(2) + F = f
• that is needed by the analytic part of the Niven proof

---