Real.pi ^ 2 is irrational #
The main result of this file is Zeta32.irrational_pi_sq.
The proof is Cartwright's integral argument, exactly as in Mathlib's
Mathlib/Analysis/Real/Pi/Irrational.lean (the definitions I, sinPoly, cosPoly and the
recursion / evaluation lemmas are copied verbatim, since they are private there). The only new
observation is Niven's: sinPoly n is an even polynomial, i.e.
sinPoly n (θ) = sinPolyY n (θ ^ 2) for an integer polynomial sinPolyY n of degree ≤ n.
Hence, at θ = π / 2 (where cos θ = 0, sin θ = 1),
I n θ * θ * (θ ^ 2) ^ n = n ! * sinPolyY n (θ ^ 2).
If θ ^ 2 = a / b with a, b > 0, then b ^ n * sinPolyY n (a / b) is an integer, equal to
a ^ n / n ! * θ * I n θ ∈ (0, 2 θ a ^ n / n !], which tends to 0: contradiction.
So π ^ 2 / 4 is irrational, hence so is π ^ 2.
π ^ 2 is irrational (Niven's variant of Cartwright's argument).