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:
- 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
if you have time
- you can prove the equality F^`(2) + F = f
- that is needed by the analytic part of the Niven proof