Lagrange's four square theorem

The main result in this file is sum_four_squares, a proof that every natural number is the sum of four square numbers.

Implementation Notes

The proof used is close to Lagrange's original proof.

theorem euler_four_squares {R : Type u_1} [CommRing R] (a b c d x y z w : R) : (a * x - b * y - c * z - d * w) ^ 2 + (a * y + b * x + c * w - d * z) ^ 2 + (a * z - b * w + c * x + d * y) ^ 2 + (a * w + b * z - c * y + d * x) ^ 2 = (a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2) * (x ^ 2 + y ^ 2 + z ^ 2 + w ^ 2)

Euler's four-square identity.

theorem Nat.euler_four_squares (a b c d x y z w : ℕ) : (↑a * ↑x - ↑b * ↑y - ↑c * ↑z - ↑d * ↑w).natAbs ^ 2 + (↑a * ↑y + ↑b * ↑x + ↑c * ↑w - ↑d * ↑z).natAbs ^ 2 + (↑a * ↑z - ↑b * ↑w + ↑c * ↑x + ↑d * ↑y).natAbs ^ 2 + (↑a * ↑w + ↑b * ↑z - ↑c * ↑y + ↑d * ↑x).natAbs ^ 2 = (a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2) * (x ^ 2 + y ^ 2 + z ^ 2 + w ^ 2)

Euler's four-square identity, a version for natural numbers.

theorem Int.sq_add_sq_of_two_mul_sq_add_sq {m x y : ℤ} (h : 2 * m = x ^ 2 + y ^ 2) : m = ((x - y) / 2) ^ 2 + ((x + y) / 2) ^ 2

theorem Int.lt_of_sum_four_squares_eq_mul {a b c d k m : ℕ} (h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = k * m) (ha : 2 * a < m) (hb : 2 * b < m) (hc : 2 * c < m) (hd : 2 * d < m) : k < m

theorem Int.exists_sq_add_sq_add_one_eq_mul (p : ℕ) [hp : Fact (Nat.Prime p)] : ∃ (a : ℕ) (b : ℕ) (k : ℕ), 0 < k ∧ k < p ∧ a ^ 2 + b ^ 2 + 1 = k * p

theorem Nat.Prime.sum_four_squares {p : ℕ} (hp : Prime p) : ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ), a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = p

Lagrange's four squares theorem for a prime number. Use Nat.sum_four_squares instead.

theorem Nat.sum_four_squares (n : ℕ) : ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ), a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = n

Four squares theorem