Sums of three squares: the case m ≡ 3 (mod 8)

This file formalises the m ≡ 3 (mod 8) case of the three-squares theorem of N. C. Ankeny: every positive integer not of the form 4ᵃ(8n + 7) is a sum of three squares. The proof follows Davenport's geometry-of-numbers argument via Minkowski's theorem (see LeanPool.SumsThreeSquares.MinkowskiConvex).

The main result is blueprint_case_mod8_eq3.

def LeanPool.SumsThreeSquares.IsSumOfThreeSquares (n : ℕ) : Prop

A number is the sum of three squares.

Equations

• LeanPool.SumsThreeSquares.IsSumOfThreeSquares n = ∃ (a : ℕ) (b : ℕ) (c : ℕ), a ^ 2 + b ^ 2 + c ^ 2 = n

theorem LeanPool.SumsThreeSquares.exists_prime_aux (m : ℕ) (hm_sq : Squarefree m) (hm_mod : m % 8 = 3) : ∃ (q : ℕ), Nat.Prime q ∧ q % 4 = 1 ∧ ∀ (p : ℕ), p ∣ m → Nat.Prime p → jacobiSym (-2 * ↑q) p = 1

A prime q ≡ 1 (mod 4) with (-2q / p) = 1 for every prime factor of m.

theorem LeanPool.SumsThreeSquares.exists_odd_sq_mod_prime_of_jacobi_eq_one (m q : ℕ) (hq_prime : Nat.Prime q) (hq_mod : q % 4 = 1) (h_jacobi : jacobiSym (-↑m) q = 1) : ∃ (b : ℤ), b ^ 2 ≡ -↑m [ZMOD ↑q] ∧ b % 2 = 1

theorem LeanPool.SumsThreeSquares.jacobi_neg_m_q (m q : ℕ) (hm_mod : m % 8 = 3) (hq_mod : q % 4 = 1) (h_jacobi : ∀ (p : ℕ), p ∣ m → Nat.Prime p → jacobiSym (-2 * ↑q) p = 1) : jacobiSym (-↑m) q = 1

theorem LeanPool.SumsThreeSquares.exists_b_h (m q : ℕ) (hm_mod : m % 8 = 3) (hq_prime : Nat.Prime q) (hq_mod : q % 4 = 1) (h_jacobi : jacobiSym (-↑m) q = 1) : ∃ (b : ℤ) (h : ℤ), b % 2 = 1 ∧ b ^ 2 - 4 * ↑q * h = -↑m

theorem LeanPool.SumsThreeSquares.exists_t (m q : ℕ) (hm_sq : Squarefree m) (hm_mod : m % 8 = 3) (hq_prime : Nat.Prime q) (h_jacobi : ∀ (p : ℕ), p ∣ m → Nat.Prime p → jacobiSym (-2 * ↑q) p = 1) : ∃ (t : ℤ), 2 * ↑q * t ^ 2 ≡ -1 [ZMOD ↑m]

noncomputable def LeanPool.SumsThreeSquares.linearMapM (m q : ℕ) (t b : ℤ) : (Fin 3 → ℝ) →ₗ[ℝ] Fin 3 → ℝ

The linear map M of the geometry-of-numbers argument.

Equations

• LeanPool.SumsThreeSquares.linearMapM m q t b = Matrix.toLin' ![![2 * ↑t * ↑q, ↑t * ↑b, ↑m], ![√(2 * ↑q), ↑b / √(2 * ↑q), 0], ![0, √↑m / √(2 * ↑q), 0]]

theorem LeanPool.SumsThreeSquares.det_linear_map_M (m q : ℕ) (t b : ℤ) (_hm : 0 < m) (hq : 0 < q) : LinearMap.det (linearMapM m q t b) = ↑m * √↑m

theorem LeanPool.SumsThreeSquares.det_linear_map_M_ne_zero (m q : ℕ) (t b : ℤ) (hm : 0 < m) (hq : 0 < q) : LinearMap.det (linearMapM m q t b) ≠ 0

@[reducible, inline]

noncomputable abbrev LeanPool.SumsThreeSquares.linearMapMEuclidean (m q : ℕ) (t b : ℤ) : EuclideanSpace ℝ (Fin 3) →ₗ[ℝ] EuclideanSpace ℝ (Fin 3)

The linear map M reinterpreted on EuclideanSpace ℝ (Fin 3).

Equations

• LeanPool.SumsThreeSquares.linearMapMEuclidean m q t b = ↑↑(EuclideanSpace.equiv (Fin 3) ℝ).symm ∘ₗ LeanPool.SumsThreeSquares.linearMapM m q t b ∘ₗ ↑↑(EuclideanSpace.equiv (Fin 3) ℝ)

theorem LeanPool.SumsThreeSquares.det_linear_map_M_euclidean (m q : ℕ) (t b : ℤ) (hm : 0 < m) (hq : 0 < q) : LinearMap.det (linearMapMEuclidean m q t b) = ↑m * √↑m

theorem LeanPool.SumsThreeSquares.vol_preimage_ball_euclidean (m q : ℕ) (t b : ℤ) (hm : 0 < m) (hq : 0 < q) : MeasureTheory.volume (⇑(linearMapMEuclidean m q t b) ⁻¹' Metric.ball 0 √(2 * ↑m)) = ENNReal.ofReal (4 / 3 * Real.pi * (2 * ↑m) ^ (3 / 2) / (↑m * √↑m))

theorem LeanPool.SumsThreeSquares.volume_inequality : 4 / 3 * Real.pi * 2 ^ (3 / 2) > 8

theorem LeanPool.SumsThreeSquares.quad_form_decomposition (m q : ℕ) (b h x y : ℤ) (hq : 0 < q) (hbqm : b ^ 2 - 4 * ↑q * h = -↑m) : (√2 * √↑q * ↑x + ↑b / (√2 * √↑q) * ↑y) ^ 2 + (√↑m / (√2 * √↑q) * ↑y) ^ 2 = 2 * (↑q * ↑x ^ 2 + ↑b * ↑x * ↑y + ↑h * ↑y ^ 2)

theorem LeanPool.SumsThreeSquares.exists_Rv_from_Minkowski (m q : ℕ) (t b h : ℤ) (hm : 0 < m) (hq : 0 < q) (hqt : t ^ 2 * 2 * ↑q ≡ -1 [ZMOD ↑m]) (hbqm : b ^ 2 - 4 * ↑q * h = -↑m) : ∃ (x : ℤ) (y : ℤ) (R : ℤ) (v : ℕ), ↑v = ↑q * x ^ 2 + b * x * y + h * y ^ 2 ∧ R ^ 2 + 2 * ↑v = ↑m ∧ 0 < v

theorem LeanPool.SumsThreeSquares.exists_R_v_of_mod8_eq3 (m : ℕ) (hm : Squarefree m) (hm_pos : 0 < m) (hmod : m % 8 = 3) : ∃ (q : ℕ) (b : ℤ) (h : ℤ) (x : ℤ) (y : ℤ) (R : ℤ) (v : ℕ), Nat.Prime q ∧ q % 4 = 1 ∧ (∀ (p : ℕ), p ∣ m → Nat.Prime p → jacobiSym (-2 * ↑q) p = 1) ∧ b ^ 2 - 4 * ↑q * h = -↑m ∧ ↑v = ↑q * x ^ 2 + b * x * y + h * y ^ 2 ∧ R ^ 2 + 2 * ↑v = ↑m ∧ 0 < v

There exist q, b, h, t, x, y, z yielding R² + 2v = m with v > 0.

theorem LeanPool.SumsThreeSquares.jacobi_neg_d_of_dvd_sq_add (p : ℕ) (a d b' : ℤ) (hp : Nat.Prime p) (_hp_odd : p ≠ 2) (hp_dvd : ↑p ∣ a ^ 2 + d * b' ^ 2) (hp_not_dvd_d : ¬↑p ∣ d) (hp_not_dvd_b : ¬↑p ∣ b') : jacobiSym (-d) p = 1

theorem LeanPool.SumsThreeSquares.jacobi_neg_d_of_odd_padicVal (p : ℕ) (a d b' : ℤ) (hp : Nat.Prime p) (hp_odd : p ≠ 2) (hp_not_dvd_d : ¬↑p ∣ d) (h_odd_val : ¬Even (padicValInt p (a ^ 2 + d * b' ^ 2))) : jacobiSym (-d) p = 1

theorem LeanPool.SumsThreeSquares.p_mod4_eq1_of_dvd_v_not_dvd_m (p : ℕ) (q b h x y v R m : ℤ) (hp : Nat.Prime p) (hp_odd : p ≠ 2) (hv : v = q * x ^ 2 + b * x * y + h * y ^ 2) (hbqm : b ^ 2 - 4 * q * h = -m) (hRv : R ^ 2 + 2 * v = m) (hpv : ¬Even (padicValInt p v)) (hpm : ¬↑p ∣ m) : p % 4 = 1

theorem LeanPool.SumsThreeSquares.p_mod4_of_dvd_v_dvd_m (p q : ℕ) (b h x y R v : ℤ) (m : ℕ) (hp : Nat.Prime p) (hp3 : p % 4 = 3) (hm_sq : Squarefree m) (hv : v = ↑q * x ^ 2 + b * x * y + h * y ^ 2) (hbqm : b ^ 2 - 4 * ↑q * h = -↑m) (hRv : R ^ 2 + 2 * v = ↑m) (hpv : ↑p ∣ v) (hpm : p ∣ m) (hjac : jacobiSym (-2 * ↑q) p = 1) : False

theorem LeanPool.SumsThreeSquares.even_padicVal_of_mod4_eq3 (p q : ℕ) (b h x y R : ℤ) (v m : ℕ) (hp : Nat.Prime p) (hp3 : p % 4 = 3) (hm_sq : Squarefree m) (hv_pos : 0 < v) (hv_def : ↑v = ↑q * x ^ 2 + b * x * y + h * y ^ 2) (hbqm : b ^ 2 - 4 * ↑q * h = -↑m) (hRv : R ^ 2 + 2 * ↑v = ↑m) (hjac : ∀ (p' : ℕ), p' ∣ m → Nat.Prime p' → jacobiSym (-2 * ↑q) p' = 1) : Even (padicValNat p (2 * v))

theorem LeanPool.SumsThreeSquares.two_v_sum_two_squares (q : ℕ) (b h x y R : ℤ) (v m : ℕ) (hm_sq : Squarefree m) (hv_pos : 0 < v) (hv_def : ↑v = ↑q * x ^ 2 + b * x * y + h * y ^ 2) (hbqm : b ^ 2 - 4 * ↑q * h = -↑m) (hRv : R ^ 2 + 2 * ↑v = ↑m) (hjac : ∀ (p : ℕ), p ∣ m → Nat.Prime p → jacobiSym (-2 * ↑q) p = 1) : ∃ (a : ℕ) (b : ℕ), 2 * v = a ^ 2 + b ^ 2

theorem LeanPool.SumsThreeSquares.blueprint_case_mod8_eq3 (m : ℕ) (hm_sq : Squarefree m) (hm_pos : 0 < m) (hm_mod : m % 8 = 3) : IsSumOfThreeSquares m

The m ≡ 3 (mod 8) case of the three-squares theorem.