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 → ∞.

@[simp]

theorem irrational_pi : Irrational Real.pi