Jacobi's two-square theorem

DefinitionDivisor sum of the character modulo 4#✓fully proved

For a natural number \(n\), this is the integer \(\sum_{d \mid n} \chi_4(d)\), the sum over the positive divisors \(d\) of \(n\) of the nonprincipal Dirichlet character \(\chi_4\) modulo 4, which takes the value \(0\) at even \(d\), \(1\) at \(d \equiv 1 \pmod 4\) and \(-1\) at \(d \equiv 3 \pmod 4\). For \(n = 0\) there are no divisors and the sum is \(0\).

public noncomputable def divChiSum (n : ℕ) : ℤ := ∑ d ∈ Nat.divisors n, ZMod.χ₄ d

Used by 6

Used byThe divisor sum of \(\chi_4\) is multiplicative · The divisor sum of \(\chi_4\) at one · The divisor sum of \(\chi_4\) at powers of a prime \(q \equiv 3 \pmod 4\) · The divisor sum of \(\chi_4\) at powers of a prime \(p \equiv 1 \pmod 4\) · The divisor sum of \(\chi_4\) at powers of two · Jacobi's two-square theorem

TheoremThe divisor sum of \(\chi_4\) is multiplicative#✓fully proved

Let \(\chi_4\) be the nonprincipal Dirichlet character modulo 4 and, for a natural number \(n\), write \(S(n) = \sum_{d \mid n} \chi_4(d)\) for the sum over the positive divisors \(d\) of \(n\) (so \(S(0) = 0\)). If \(m\) and \(n\) are coprime natural numbers, then \(S(mn) = S(m)\,S(n)\).

public theorem divChiSum_mul_of_coprime {m n : ℕ} (h : Nat.Coprime m n) :
    divChiSum (m * n) = divChiSum m * divChiSum n

Uses 1 · Used by 1

Statement usesDivisor sum of the character modulo 4

Used byJacobi's two-square theorem

TheoremThe divisor sum of \(\chi_4\) at one#✓fully proved

For the nonprincipal Dirichlet character \(\chi_4\) modulo 4, the sum \(\sum_{d \mid 1} \chi_4(d)\) over the divisors of \(1\) equals \(1\).

public theorem divChiSum_one : divChiSum 1 = 1

Uses 1 · Used by 1

Statement usesDivisor sum of the character modulo 4

Used byJacobi's two-square theorem

TheoremThe divisor sum of \(\chi_4\) at powers of two#✓fully proved

Let \(\chi_4\) be the nonprincipal Dirichlet character modulo 4. For every natural number \(e\), \(\sum_{d \mid 2^e} \chi_4(d) = 1\): only the divisor \(1\) contributes.

public theorem divChiSum_prime_pow_two (e : ℕ) : divChiSum (2 ^ e) = 1

Uses 1 · Used by 1

Statement usesDivisor sum of the character modulo 4

Used byJacobi's two-square theorem

TheoremThe divisor sum of \(\chi_4\) at powers of a prime \(p \equiv 1 \pmod 4\)#✓fully proved

Let \(\chi_4\) be the nonprincipal Dirichlet character modulo 4. If \(p\) is a prime with \(p \equiv 1 \pmod 4\) and \(e\) is a natural number, then \(\sum_{d \mid p^e} \chi_4(d) = e + 1\).

public theorem divChiSum_prime_pow_split {p e : ℕ} (hp : p.Prime)
    (h : p % 4 = 1) : divChiSum (p ^ e) = ((e + 1 : ℕ) : ℤ)

Uses 1 · Used by 1

Statement usesDivisor sum of the character modulo 4

Used byJacobi's two-square theorem

TheoremThe divisor sum of \(\chi_4\) at powers of a prime \(q \equiv 3 \pmod 4\)#✓fully proved

Let \(\chi_4\) be the nonprincipal Dirichlet character modulo 4. If \(q\) is a prime with \(q \equiv 3 \pmod 4\) and \(f\) is a natural number, then \(\sum_{d \mid q^f} \chi_4(d)\) equals \(1\) when \(f\) is even and \(0\) when \(f\) is odd.

public theorem divChiSum_prime_pow_inert {q f : ℕ} (hp : q.Prime)
    (h : q % 4 = 3) : divChiSum (q ^ f) = if Even f then 1 else 0

Uses 1 · Used by 1

Statement usesDivisor sum of the character modulo 4

Used byJacobi's two-square theorem

DefinitionSums of two squares as Gaussian norms#✓fully proved

For a natural number \(j\), the map \((a, b) \mapsto a + bi\) is a bijection from the set of integer pairs \((a, b)\) with \(a^2 + b^2 = j\) to the set of Gaussian integers \(z\) with norm \(N(z) = j\); its inverse sends \(z\) to the pair of its real and imaginary parts.

SumSquares.pairEquivGaussianNormFiber · 18 lines

public def pairEquivGaussianNormFiber (j : ℕ) :
    {p : ℤ × ℤ // p.1 ^ 2 + p.2 ^ 2 = (j : ℤ)} ≃
      {z : ℤ[i] // (Zsqrtd.norm z).natAbs = j} where
  toFun p := ⟨⟨p.1.1, p.1.2⟩, by
    have hnorm : Zsqrtd.norm (⟨p.1.1, p.1.2⟩ : ℤ[i]) =
        p.1.1 ^ 2 + p.1.2 ^ 2 := by
      rw [Zsqrtd.norm_def]
      dsimp only
      ring
    rw [hnorm, p.2, Int.natAbs_natCast]⟩
  invFun z := ⟨(z.1.re, z.1.im), by
    have hnonneg : 0 ≤ Zsqrtd.norm z.1 := GaussianInt.norm_nonneg z.1
    have hnorm : Zsqrtd.norm z.1 = (j : ℤ) := by
      rw [← Int.natAbs_of_nonneg hnonneg, z.2]
    rw [Zsqrtd.norm_def] at hnorm
    simpa [pow_two] using hnorm⟩
  left_inv p := Subtype.ext rfl
  right_inv z := Subtype.ext rfl

Used by 2

Used byTwo-square representation numbers count integer pairs · Jacobi's two-square theorem

TheoremTwo-square representation numbers count integer pairs#✓fully proved

For every natural number \(j\), the representation number \(r_2(j)\) equals the number of pairs \((a, b)\) of integers with \(a^2 + b^2 = j\).

public theorem representationNumber_two_eq (j : ℕ) :
    SumSquares.representationNumber 2 j =
      Fintype.card {p : ℤ × ℤ // p.1 ^ 2 + p.2 ^ 2 = (j : ℤ)}

Uses 3 · Used by 1

Statement usesSums of two squares as Gaussian norms · Representation numbers of sums of squares

Proof usesInteger solutions of a sum of squares

Used byJacobi's two-square theorem

TheoremJacobi's two-square theorem#✓fully proved

Let \(\chi_4\) be the nonprincipal Dirichlet character modulo \(4\), so \(\chi_4(d)\) is \(0\) for even \(d\), \(1\) for \(d \equiv 1 \pmod 4\) and \(-1\) for \(d \equiv 3 \pmod 4\). For every natural number \(j \ge 1\), the representation number \(r_2(j)\), the number of integer pairs \((x_1, x_2)\) with \(x_1^2 + x_2^2 = j\) counted with order and signs, satisfies \(r_2(j) = 4 \sum_{d \mid j} \chi_4(d)\), where \(d\) runs over the positive divisors of \(j\).

public theorem representationNumber_two_jacobi_count (j : ℕ) (hj : 1 ≤ j) :
    (SumSquares.representationNumber 2 j : ℤ) =
      4 * ∑ d ∈ j.divisors, ZMod.χ₄ d

Uses 21

Statement usesRepresentation numbers of sums of squares

Proof usesNumber of Gaussian integers of norm a power of a split prime · 1 + i is a Gaussian prime · Primes congruent to 1 mod 4 split in the Gaussian integers · Factorization of 2 in the Gaussian integers · Enumeration of the Gaussian units · Inverses of the Gaussian units · The enumeration of the Gaussian units is complete · The four Gaussian units are distinct · Each Gaussian unit times its listed inverse is one · Divisor sum of the character modulo 4 · The divisor sum of \(\chi_4\) is multiplicative · The divisor sum of \(\chi_4\) at one · The divisor sum of \(\chi_4\) at powers of a prime \(q \equiv 3 \pmod 4\) · The divisor sum of \(\chi_4\) at powers of a prime \(p \equiv 1 \pmod 4\) · The divisor sum of \(\chi_4\) at powers of two · Sums of two squares as Gaussian norms · Two-square representation numbers count integer pairs · Norm counts determined by prime powers · Norm counts at an inert prime · Norm counts at powers of a ramified two

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.