`Real.pi`

is irrational #

The main result of this file is `irrational_pi`

.

The proof is adapted from https://en.wikipedia.org/wiki/Proof_that_%CF%80_is_irrational#Cartwright's_proof.

The proof idea is as follows.

- Define a sequence of integrals
`I n θ = ∫ x in (-1)..1, (1 - x ^ 2) ^ n * cos (x * θ)`

. - Give a recursion formula for
`I (n + 2) θ * θ ^ 2`

in terms of`I n θ`

and`I (n + 1) θ`

. Note we do not find it helpful to define`J`

as in the above proof, and instead work directly with`I`

. - Define polynomials with integer coefficients
`sinPoly n`

and`cosPoly n`

such that`I n θ * θ ^ (2 * n + 1) = n ! * (sinPoly n θ * sin θ + cosPoly n θ * cos θ)`

. Note that in the informal proof, these polynomials are not defined explicitly, but we find it useful to define them by recursion. - Show that both these polynomials have degree bounded by
`n`

. - Show that
`0 < I n (π / 2) ≤ 2`

for all`n`

. - Now we can finish: if
`π / 2`

is rational, write it as`a / b`

with`a, b > 0`

. Then`b ^ (2 * n + 1) * sinPoly n (a / b)`

is a positive integer by the degree bound. But it is equal to`a ^ (2 * n + 1) / n ! * I n (π / 2) ≤ 2 * a * (2 * n + 1) / n !`

, which converges to 0 as`n → ∞`

.