From irrationality of ζ(3) - r ζ(2) to ℚ-linear independence of 1, ζ(2), ζ(3)

Main result: Zeta32.LinearIndependence.linearIndependent_of_irrational.

• riemannZeta k (for k ≥ 2) is the complexification of the real series ∑' n : ℕ, 1 / ((n : ℝ) + 1) ^ k (riemannZeta_nat_eq_ofReal_tsum).
• ζ(2) = π ^ 2 / 6 is irrational, by Zeta32.irrational_pi_sq.
• A rational relation a + b ζ(2) + c ζ(3) = 0 with c ≠ 0 makes ζ(3) - (-b / c) ζ(2) = -a / c rational; with c = 0, b ≠ 0 it makes ζ(2) rational; with b = c = 0 it forces a = 0.

theorem Zeta32.LinearIndependence.riemannZeta_nat_eq_ofReal_tsum {k : ℕ} (hk : 1 < k) : riemannZeta ↑k = ↑(∑' (n : ℕ), 1 / (↑n + 1) ^ k)

For k ≥ 2, riemannZeta k is the complexification of ∑' n, 1 / (n + 1) ^ k over ℝ.

theorem Zeta32.LinearIndependence.riemannZeta_two_eq_ofReal_tsum : riemannZeta 2 = ↑(∑' (n : ℕ), 1 / (↑n + 1) ^ 2)

theorem Zeta32.LinearIndependence.riemannZeta_three_eq_ofReal_tsum : riemannZeta 3 = ↑(∑' (n : ℕ), 1 / (↑n + 1) ^ 3)

theorem Zeta32.LinearIndependence.tsum_two_eq : ∑' (n : ℕ), 1 / (↑n + 1) ^ 2 = Real.pi ^ 2 / 6

∑' n, 1 / (n + 1) ^ 2 = π ^ 2 / 6.

theorem Zeta32.LinearIndependence.irrational_tsum_two : Irrational (∑' (n : ℕ), 1 / (↑n + 1) ^ 2)

ζ(2) = ∑' n, 1 / (n + 1) ^ 2 is irrational.

theorem Zeta32.LinearIndependence.linearIndependent_of_irrational : (∀ (r : ℚ), Irrational (∑' (k : ℕ), 1 / (↑k + 1) ^ 3 - ↑r * ∑' (k : ℕ), 1 / (↑k + 1) ^ 2)) → LinearIndependent ℚ ![1, riemannZeta 2, riemannZeta 3]