To play this document inside your browser use ALT-N and ALT-P. If you get stack overflow errors, try to use Google Chrome or Chromium with the command line option --js-flags="--harmony-tailcalls".

You can save your edits inside your browser and load them back (edits are also saved when you close the window). Finally you can download the file for offline editing.


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