Representation numbers of sums of squares

DefinitionInteger solutions of a sum of squares#✓fully proved

For natural numbers \(k\) and \(n\), the solution set is the set of all integer vectors \(x = (x_1, \dots, x_k) \in \mathbb{Z}^k\) with \(x_1^2 + \cdots + x_k^2 = n\).

def solutions (k n : ℕ) : Set (Fin k → ℤ) :=
  { x | dotProduct x x = (n : ℤ) }

Used by 11

Used byTwo-square representation numbers count integer pairs · Representation numbers of sums of squares · The representation number counts a finite set · Zero as a sum of one square · Positive integers have no representation as a sum of zero squares · Zero as a sum of zero squares · Finitely many representations as a sum of squares · Solution set of one square equal to zero · Zero squares never sum to a positive integer · Solution set of the empty sum at zero · The zero vector represents zero as a sum of squares

DefinitionRepresentation numbers of sums of squares#✓fully proved

For natural numbers \(k\) and \(n\), the representation number \(r_k(n)\) is the number of elements of the solution set, that is, the number of integer vectors \((x_1, \dots, x_k) \in \mathbb{Z}^k\) with \(x_1^2 + \cdots + x_k^2 = n\). Representations that differ in the order or the signs of the entries are counted separately.

noncomputable def representationNumber (k n : ℕ) : ℕ :=
  (solutions k n).ncard

Uses 1 · Used by 6

Statement usesInteger solutions of a sum of squares

Used byTwo-square representation numbers count integer pairs · Jacobi's two-square theorem · The representation number counts a finite set · Zero as a sum of one square · Positive integers have no representation as a sum of zero squares · Zero as a sum of zero squares

TheoremFinitely many representations as a sum of squares#✓fully proved

For all natural numbers \(k\) and \(n\), there are only finitely many integer vectors \((x_1, \dots, x_k) \in \mathbb{Z}^k\) with \(x_1^2 + \cdots + x_k^2 = n\).

theorem solutions_finite (k n : ℕ) : Set.Finite (solutions k n)

Uses 1 · Used by 1

Statement usesInteger solutions of a sum of squares

Used byThe representation number counts a finite set

TheoremThe representation number counts a finite set#✓fully proved

For all natural numbers \(k\) and \(n\), the representation number \(r_k(n)\) equals the number of elements of the finite solution set of integer vectors \((x_1, \dots, x_k) \in \mathbb{Z}^k\) with \(x_1^2 + \cdots + x_k^2 = n\).

theorem representationNumber_eq_toFinset_card (k n : ℕ) :
    representationNumber k n = (solutions_finite k n).toFinset.card

Uses 3

Statement usesRepresentation numbers of sums of squares · Integer solutions of a sum of squares · Finitely many representations as a sum of squares

TheoremThe zero vector represents zero as a sum of squares#✓fully proved

For every \(k \in \mathbb{N}\), the zero vector of \(\mathbb{Z}^k\) has squared norm \(0\), that is, it lies in the set of integer vectors \(x \in \mathbb{Z}^k\) with \(x_1^2 + \cdots + x_k^2 = 0\).

theorem zero_mem_solutions (k : ℕ) :
    (0 : Fin k → ℤ) ∈ solutions k 0

Uses 1

Statement usesInteger solutions of a sum of squares

TheoremSolution set of the empty sum at zero#✓fully proved

The set of vectors \(x \in \mathbb{Z}^0\) whose sum of squares (an empty sum) equals \(0\) is all of \(\mathbb{Z}^0\).

theorem solutions_zero_zero : solutions 0 0 = Set.univ

Uses 1 · Used by 1

Statement usesInteger solutions of a sum of squares

Used byZero as a sum of zero squares

TheoremZero squares never sum to a positive integer#✓fully proved

For every natural number \(n \ge 1\), no vector \(x \in \mathbb{Z}^0\) has sum of squares equal to \(n\); that is, the solution set is empty.

theorem solutions_zero_succ (n : ℕ) : solutions 0 (n + 1) = ∅

Uses 1 · Used by 1

Statement usesInteger solutions of a sum of squares

Used byPositive integers have no representation as a sum of zero squares

TheoremSolution set of one square equal to zero#✓fully proved

The set of vectors \(x \in \mathbb{Z}^1\) with \(x_1^2 = 0\) consists of the zero vector alone.

theorem solutions_one_zero : solutions 1 0 = {(0 : Fin 1 → ℤ)}

Uses 1 · Used by 1

Statement usesInteger solutions of a sum of squares

Used byZero as a sum of one square

TheoremZero as a sum of zero squares#✓fully proved

The representation number \(r_0(0)\), the number of integer vectors \(x \in \mathbb{Z}^0\) whose sum of squares (an empty sum) equals \(0\), is \(1\).

theorem representationNumber_zero_zero : representationNumber 0 0 = 1

Uses 3

Statement usesRepresentation numbers of sums of squares

Proof usesInteger solutions of a sum of squares · Solution set of the empty sum at zero

TheoremPositive integers have no representation as a sum of zero squares#✓fully proved

For every natural number \(n \ge 1\), the representation number \(r_0(n)\), the number of integer vectors \(x \in \mathbb{Z}^0\) whose sum of squares (an empty sum) equals \(n\), is \(0\).

theorem representationNumber_zero_succ (n : ℕ) :
    representationNumber 0 (n + 1) = 0

Uses 3

Statement usesRepresentation numbers of sums of squares

Proof usesInteger solutions of a sum of squares · Zero squares never sum to a positive integer

TheoremZero as a sum of one square#✓fully proved

The representation number \(r_1(0)\), the number of integer vectors \(x \in \mathbb{Z}^1\) with \(x_1^2 = 0\), equals \(1\).

theorem representationNumber_one_zero : representationNumber 1 0 = 1

Uses 3

Statement usesRepresentation numbers of sums of squares

Proof usesInteger solutions of a sum of squares · Solution set of one square equal to zero

11 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.