Representations by x² + 2y²

TheoremThe character \(\chi_{-2}\) takes the value \(1\) at \(1\)#✓fully proved

Let \(\chi_{-2}\) be the quadratic character modulo \(8\) with values in \(\mathbb{Z}\) (the character of \(\mathbb{Q}(\sqrt{-2})\)): \(\chi_{-2}(n) = 1\) for \(n \equiv 1, 3 \pmod 8\), \(\chi_{-2}(n) = -1\) for \(n \equiv 5, 7 \pmod 8\), and \(\chi_{-2}(n) = 0\) for even \(n\). Then \(\chi_{-2}(1) = 1\).

public theorem chiNeg2_one : ZMod.χ₈' 1 = 1

Used by 1

Used byThe divisor sum of \(\chi_{-2}\) at \(1\)

DefinitionDivisor sum of the character \(\chi_{-2}\)#✓fully proved

Let \(\chi_{-2}\) be the quadratic character modulo \(8\) with values in \(\mathbb{Z}\) (the character of \(\mathbb{Q}(\sqrt{-2})\)): \(\chi_{-2}(n) = 1\) for \(n \equiv 1, 3 \pmod 8\), \(\chi_{-2}(n) = -1\) for \(n \equiv 5, 7 \pmod 8\), and \(\chi_{-2}(n) = 0\) for even \(n\). For a natural number \(t\), the divisor sum of \(\chi_{-2}\) at \(t\) is the integer \(\sum_{d \mid t} \chi_{-2}(d)\), the sum over the positive divisors \(d\) of \(t\). By convention \(0\) has no divisors here, so the divisor sum at \(t = 0\) is \(0\).

public noncomputable def divChiNeg2Sum (t : ℕ) : ℤ :=
  ∑ d ∈ Nat.divisors t, ZMod.χ₈' d

Used by 8

Used byMultiplicativity of the divisor sum of \(\chi_{-2}\) · The divisor sum of \(\chi_{-2}\) at \(1\) · The divisor sum of \(\chi_{-2}\) at powers of a prime \(q \equiv 5, 7 \pmod 8\) · The divisor sum of \(\chi_{-2}\) at powers of a prime \(p \equiv 1, 3 \pmod 8\) · The divisor sum of \(\chi_{-2}\) at powers of \(2\) · Doubling an odd argument leaves the divisor sum of \(\chi_{-2}\) unchanged · Number of representations by \(x^2 + 2y^2\) · Elements of \(\mathbb{Z}(\sqrt{-2})\) of norm \(t\) counted by a divisor sum

TheoremMultiplicativity of the divisor sum of \(\chi_{-2}\)#✓fully proved

Let \(\chi_{-2}\) be the quadratic character modulo \(8\) with \(\chi_{-2}(n) = 1\) for \(n \equiv 1, 3 \pmod 8\), \(\chi_{-2}(n) = -1\) for \(n \equiv 5, 7 \pmod 8\) and \(\chi_{-2}(n) = 0\) for even \(n\). For a natural number \(t\), let \(S(t) = \sum_{d \mid t} \chi_{-2}(d)\), the sum over the positive divisors \(d\) of \(t\), with \(S(0) = 0\) (the empty sum). For coprime natural numbers \(m\) and \(n\), \(S(mn) = S(m)\,S(n)\).

The proof uses that \(\chi_{-2}\) is completely multiplicative.

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

Uses 1 · Used by 2

Statement usesDivisor sum of the character \(\chi_{-2}\)

Used byDoubling an odd argument leaves the divisor sum of \(\chi_{-2}\) unchanged · Elements of \(\mathbb{Z}(\sqrt{-2})\) of norm \(t\) counted by a divisor sum

TheoremThe divisor sum of \(\chi_{-2}\) at \(1\)#✓fully proved

Let \(\chi_{-2}\) be the quadratic character modulo \(8\) with \(\chi_{-2}(n) = 1\) for \(n \equiv 1, 3 \pmod 8\), \(\chi_{-2}(n) = -1\) for \(n \equiv 5, 7 \pmod 8\) and \(\chi_{-2}(n) = 0\) for even \(n\). For a positive integer \(t\), let \(S(t) = \sum_{d \mid t} \chi_{-2}(d)\), the sum over the positive divisors \(d\) of \(t\). Then \(S(1) = 1\).

public theorem divChiNeg2Sum_one : divChiNeg2Sum 1 = 1

Uses 2 · Used by 1

Statement usesDivisor sum of the character \(\chi_{-2}\)

Proof usesThe character \(\chi_{-2}\) takes the value \(1\) at \(1\)

Used byElements of \(\mathbb{Z}(\sqrt{-2})\) of norm \(t\) counted by a divisor sum

TheoremThe divisor sum of \(\chi_{-2}\) at powers of \(2\)#✓fully proved

Let \(\chi_{-2}\) be the quadratic character modulo \(8\) with \(\chi_{-2}(n) = 1\) for \(n \equiv 1, 3 \pmod 8\), \(\chi_{-2}(n) = -1\) for \(n \equiv 5, 7 \pmod 8\) and \(\chi_{-2}(n) = 0\) for even \(n\). For a positive integer \(t\), let \(S(t) = \sum_{d \mid t} \chi_{-2}(d)\), the sum over the positive divisors \(d\) of \(t\). For every natural number \(e\), \(S(2^e) = 1\): only the divisor \(1\) contributes.

public theorem divChiNeg2Sum_prime_pow_two (e : ℕ) :
    divChiNeg2Sum (2 ^ e) = 1

Uses 1 · Used by 2

Statement usesDivisor sum of the character \(\chi_{-2}\)

Used byDoubling an odd argument leaves the divisor sum of \(\chi_{-2}\) unchanged · Elements of \(\mathbb{Z}(\sqrt{-2})\) of norm \(t\) counted by a divisor sum

TheoremThe divisor sum of \(\chi_{-2}\) at powers of a prime \(p \equiv 1, 3 \pmod 8\)#✓fully proved

Let \(\chi_{-2}\) be the quadratic character modulo \(8\) with \(\chi_{-2}(n) = 1\) for \(n \equiv 1, 3 \pmod 8\), \(\chi_{-2}(n) = -1\) for \(n \equiv 5, 7 \pmod 8\) and \(\chi_{-2}(n) = 0\) for even \(n\). For a positive integer \(t\), let \(S(t) = \sum_{d \mid t} \chi_{-2}(d)\), the sum over the positive divisors \(d\) of \(t\). If \(p\) is a prime with \(p \equiv 1 \pmod 8\) or \(p \equiv 3 \pmod 8\), then \(S(p^e) = e + 1\) for every natural number \(e\): every divisor of \(p^e\) contributes \(1\).

public theorem divChiNeg2Sum_prime_pow_split {p e : ℕ} (hp : p.Prime)
    (h : p % 8 = 1 ∨ p % 8 = 3) :
    divChiNeg2Sum (p ^ e) = ((e + 1 : ℕ) : ℤ)

Uses 1 · Used by 1

Statement usesDivisor sum of the character \(\chi_{-2}\)

Used byElements of \(\mathbb{Z}(\sqrt{-2})\) of norm \(t\) counted by a divisor sum

TheoremThe divisor sum of \(\chi_{-2}\) at powers of a prime \(q \equiv 5, 7 \pmod 8\)#✓fully proved

Let \(\chi_{-2}\) be the quadratic character modulo \(8\) with \(\chi_{-2}(n) = 1\) for \(n \equiv 1, 3 \pmod 8\), \(\chi_{-2}(n) = -1\) for \(n \equiv 5, 7 \pmod 8\) and \(\chi_{-2}(n) = 0\) for even \(n\). For a positive integer \(t\), let \(S(t) = \sum_{d \mid t} \chi_{-2}(d)\), the sum over the positive divisors \(d\) of \(t\). If \(q\) is a prime with \(q \equiv 5 \pmod 8\) or \(q \equiv 7 \pmod 8\), then for every natural number \(f\), \(S(q^f) = 1\) if \(f\) is even and \(S(q^f) = 0\) if \(f\) is odd.

public theorem divChiNeg2Sum_prime_pow_inert {q f : ℕ} (hp : q.Prime)
    (h : q % 8 = 5 ∨ q % 8 = 7) :
    divChiNeg2Sum (q ^ f) = if Even f then 1 else 0

Uses 1 · Used by 1

Statement usesDivisor sum of the character \(\chi_{-2}\)

Used byElements of \(\mathbb{Z}(\sqrt{-2})\) of norm \(t\) counted by a divisor sum

DefinitionNumber of elements of \(\mathbb{Z}(\sqrt{-2})\) of a given norm#✓fully proved

For a natural number \(t\), the representation count of \(t\) is the number of elements \(z = a + b\sqrt{-2}\) of \(\mathbb{Z}[\sqrt{-2}]\), with \(a, b\) integers, whose norm \(N(z) = a^2 + 2b^2\) has absolute value \(t\). Since the norm is never negative, this is the number of elements of norm \(t\).

public noncomputable def repX2Y2Count (t : ℕ) : ℕ :=
  Fintype.card {z : ℤ√(-2 : ℤ) // (Zsqrtd.norm z).natAbs = t}

Used by 7

Used byCounting representations by \(x^2 + 2y^2\) through positive solutions · Elements of \(\mathbb{Z}(\sqrt{-2})\) whose norm is a power of an inert prime · Elements of norm one in \(\mathbb{Z}(\sqrt{-2})\) · Elements of \(\mathbb{Z}(\sqrt{-2})\) whose norm is a power of a split prime · Elements of \(\mathbb{Z}(\sqrt{-2})\) whose norm is a power of \(2\) · Number of representations by \(x^2 + 2y^2\) · Elements of \(\mathbb{Z}(\sqrt{-2})\) of norm \(t\) counted by a divisor sum

TheoremElements of norm one in \(\mathbb{Z}(\sqrt{-2})\)#✓fully proved

Exactly two elements \(a + b\sqrt{-2}\) of \(\mathbb{Z}[\sqrt{-2}]\), with \(a, b\) integers, have norm \(a^2 + 2b^2 = 1\).

These are the units \(\pm 1\).

public theorem repX2Y2Count_one : repX2Y2Count 1 = 2

Uses 10

Statement usesNumber of elements of \(\mathbb{Z}(\sqrt{-2})\) of a given norm

Proof usesRounding division on \(\mathbb{Z}(\sqrt{-2})\) · The remainder is smaller than the divisor, in absolute norm · Multiplying by a nonzero element does not decrease the norm in \(\mathbb{Z}(\sqrt{-2})\) · Enumeration of the units of ℤ(√−2) · Inverses of the enumerated units of ℤ(√−2) · Every unit of ℤ(√−2) is enumerated · The enumeration of the units of ℤ(√−2) is injective · Each enumerated unit of ℤ(√−2) times its listed inverse is one · Counting a norm class generated by one element

TheoremElements of \(\mathbb{Z}(\sqrt{-2})\) whose norm is a power of \(2\)#✓fully proved

For every natural number \(e\), exactly two elements \(a + b\sqrt{-2}\) of \(\mathbb{Z}[\sqrt{-2}]\), with \(a, b\) integers, have norm \(a^2 + 2b^2 = 2^e\).

The prime \(2\) is ramified in \(\mathbb{Z}[\sqrt{-2}]\).

public theorem repX2Y2Count_two_pow (e : ℕ) : repX2Y2Count (2 ^ e) = 2

Uses 12 · Used by 1

Statement usesNumber of elements of \(\mathbb{Z}(\sqrt{-2})\) of a given norm

Proof usesRounding division on \(\mathbb{Z}(\sqrt{-2})\) · The remainder is smaller than the divisor, in absolute norm · Multiplying by a nonzero element does not decrease the norm in \(\mathbb{Z}(\sqrt{-2})\) · Enumeration of the units of ℤ(√−2) · Inverses of the enumerated units of ℤ(√−2) · Every unit of ℤ(√−2) is enumerated · The enumeration of the units of ℤ(√−2) is injective · Each enumerated unit of ℤ(√−2) times its listed inverse is one · Units of ℤ(√−2) · √−2 is prime in ℤ(√−2) · Norm counts at powers of a ramified two

Used byElements of \(\mathbb{Z}(\sqrt{-2})\) of norm \(t\) counted by a divisor sum

TheoremElements of \(\mathbb{Z}(\sqrt{-2})\) whose norm is a power of an inert prime#✓fully proved

Let \(q\) be a prime with \(q \equiv 5\) or \(q \equiv 7 \pmod 8\), and let \(f\) be a natural number. The number of elements \(a + b\sqrt{-2}\) of \(\mathbb{Z}[\sqrt{-2}]\), with \(a, b\) integers, of norm \(a^2 + 2b^2 = q^f\) is \(2\) if \(f\) is even and \(0\) if \(f\) is odd.

public theorem repX2Y2Count_inert_pow {q f : ℕ} [Fact q.Prime]
    (h : q % 8 = 5 ∨ q % 8 = 7) :
    repX2Y2Count (q ^ f) = if Even f then 2 else 0

Uses 11 · Used by 1

Statement usesNumber of elements of \(\mathbb{Z}(\sqrt{-2})\) of a given norm

Proof usesRounding division on \(\mathbb{Z}(\sqrt{-2})\) · The remainder is smaller than the divisor, in absolute norm · Multiplying by a nonzero element does not decrease the norm in \(\mathbb{Z}(\sqrt{-2})\) · Enumeration of the units of ℤ(√−2) · Inverses of the enumerated units of ℤ(√−2) · Every unit of ℤ(√−2) is enumerated · The enumeration of the units of ℤ(√−2) is injective · Each enumerated unit of ℤ(√−2) times its listed inverse is one · Primes congruent to 5 or 7 mod 8 are inert in ℤ(√−2) · Norm counts at an inert prime

Used byElements of \(\mathbb{Z}(\sqrt{-2})\) of norm \(t\) counted by a divisor sum

TheoremElements of \(\mathbb{Z}(\sqrt{-2})\) whose norm is a power of a split prime#✓fully proved

Write \(N(a + b\sqrt{-2}) = a^2 + 2b^2\) for the norm of an element of \(\mathbb{Z}[\sqrt{-2}]\), where \(a, b\) are integers. Let \(p\) be a prime with \(p \equiv 1\) or \(p \equiv 3 \pmod 8\), and suppose \(\pi\) is a prime element of \(\mathbb{Z}[\sqrt{-2}]\) with \(N(\pi) = p\). Then for every natural number \(e\), the number of elements of \(\mathbb{Z}[\sqrt{-2}]\) of norm \(p^e\) is \(2(e + 1)\).

public theorem repX2Y2Count_split_pow {p e : ℕ} [Fact p.Prime]
    (h : p % 8 = 1 ∨ p % 8 = 3) {π : ℤ√(-2 : ℤ)}
    (hnorm : Zsqrtd.norm π = p) (hprime : Prime π) :
    repX2Y2Count (p ^ e) = 2 * (e + 1)

Uses 11 · Used by 1

Statement usesNumber of elements of \(\mathbb{Z}(\sqrt{-2})\) of a given norm

Proof usesRounding division on \(\mathbb{Z}(\sqrt{-2})\) · The remainder is smaller than the divisor, in absolute norm · Multiplying by a nonzero element does not decrease the norm in \(\mathbb{Z}(\sqrt{-2})\) · Enumeration of the units of ℤ(√−2) · Inverses of the enumerated units of ℤ(√−2) · Every unit of ℤ(√−2) is enumerated · The enumeration of the units of ℤ(√−2) is injective · Each enumerated unit of ℤ(√−2) times its listed inverse is one · Conjugate factorization of an odd prime in \(\mathbb{Z}(\sqrt{-2})\) · Norm counts at a split prime

Used byElements of \(\mathbb{Z}(\sqrt{-2})\) of norm \(t\) counted by a divisor sum

TheoremElements of \(\mathbb{Z}(\sqrt{-2})\) of norm \(t\) counted by a divisor sum#✓fully proved

For every positive integer \(t\), the number of elements \(a + b\sqrt{-2}\) of \(\mathbb{Z}[\sqrt{-2}]\), with \(a, b\) integers, of norm \(a^2 + 2b^2 = t\) equals \(2 \sum_{d \mid t} \chi(d)\), where \(d\) runs over the positive divisors of \(t\) and \(\chi\) is the character modulo \(8\) given by \(\chi(d) = 1\) if \(d \equiv 1, 3 \pmod 8\), \(\chi(d) = -1\) if \(d \equiv 5, 7 \pmod 8\), and \(\chi(d) = 0\) if \(d\) is even.

Equivalently, this counts the integer pairs \((x, y)\) with \(x^2 + 2y^2 = t\).

public theorem x2y2_count {t : ℕ} (ht : t ≠ 0) :
    (repX2Y2Count t : ℤ) = 2 * divChiNeg2Sum t

Uses 20 · Used by 1

Statement usesDivisor sum of the character \(\chi_{-2}\) · Number of elements of \(\mathbb{Z}(\sqrt{-2})\) of a given norm

Proof usesMultiplicativity of the divisor sum of \(\chi_{-2}\) · The divisor sum of \(\chi_{-2}\) at \(1\) · The divisor sum of \(\chi_{-2}\) at powers of a prime \(q \equiv 5, 7 \pmod 8\) · The divisor sum of \(\chi_{-2}\) at powers of a prime \(p \equiv 1, 3 \pmod 8\) · The divisor sum of \(\chi_{-2}\) at powers of \(2\) · Elements of \(\mathbb{Z}(\sqrt{-2})\) whose norm is a power of an inert prime · Elements of \(\mathbb{Z}(\sqrt{-2})\) whose norm is a power of a split prime · Elements of \(\mathbb{Z}(\sqrt{-2})\) whose norm is a power of \(2\) · Rounding division on \(\mathbb{Z}(\sqrt{-2})\) · The remainder is smaller than the divisor, in absolute norm · Multiplying by a nonzero element does not decrease the norm in \(\mathbb{Z}(\sqrt{-2})\) · Enumeration of the units of ℤ(√−2) · Inverses of the enumerated units of ℤ(√−2) · Every unit of ℤ(√−2) is enumerated · The enumeration of the units of ℤ(√−2) is injective · Each enumerated unit of ℤ(√−2) times its listed inverse is one · Primes \(p \equiv 1, 3 \pmod 8\) are norms of primes of \(\mathbb{Z}(\sqrt{-2})\) · Norm counts determined by prime powers

Used byNumber of representations by \(x^2 + 2y^2\)

TheoremCoordinates of an element of norm \(N\) in \(\mathbb{Z}(\sqrt{-2})\)#✓fully proved

Let \(N\) be a natural number and let \(z = a + b\sqrt{-2}\), with \(a, b \in \mathbb{Z}\), be an element of \(\mathbb{Z}[\sqrt{-2}]\) whose norm has absolute value \(N\). Then \(a^2 + 2b^2 = N\).

public theorem re_mul_re_add_two_mul_im_mul_im {N : ℕ} {z : ℤ√(-2 : ℤ)}
    (hz : (Zsqrtd.norm z).natAbs = N) :
    z.re * z.re + 2 * (z.im * z.im) = (N : ℤ)

Used by 1

Used byCounting representations by \(x^2 + 2y^2\) through positive solutions

TheoremCounting representations by \(x^2 + 2y^2\) through positive solutions#✓fully proved

Let \(N\) be a natural number such that every element \(a + b\sqrt{-2}\) of \(\mathbb{Z}[\sqrt{-2}]\) of norm \(a^2 + 2b^2 = N\) has \(a \neq 0\) and \(b \neq 0\). Then the number of elements of \(\mathbb{Z}[\sqrt{-2}]\) of norm \(N\) is four times the number of pairs \((x, y)\) of positive integers with \(x^2 + 2y^2 = N\).

public theorem repX2Y2Count_eq_four_mul_pos (N : ℕ)
    (hre : ∀ z : ℤ√(-2 : ℤ), (Zsqrtd.norm z).natAbs = N → z.re ≠ 0)
    (him : ∀ z : ℤ√(-2 : ℤ), (Zsqrtd.norm z).natAbs = N → z.im ≠ 0) :
    repX2Y2Count N = 4 * (((Finset.Icc 1 N ×ˢ Finset.Icc 1 N).filter
      (fun p : ℕ × ℕ => p.1 ^ 2 + 2 * p.2 ^ 2 = N ∧ 0 < p.1 ∧ 0 < p.2))).card

Uses 2

Statement usesNumber of elements of \(\mathbb{Z}(\sqrt{-2})\) of a given norm

Proof usesCoordinates of an element of norm \(N\) in \(\mathbb{Z}(\sqrt{-2})\)

TheoremDoubling an odd argument leaves the divisor sum of \(\chi_{-2}\) unchanged#✓fully proved

Let \(\chi_{-2}\) be the quadratic character modulo \(8\) with \(\chi_{-2}(n) = 1\) for \(n \equiv 1, 3 \pmod 8\), \(\chi_{-2}(n) = -1\) for \(n \equiv 5, 7 \pmod 8\) and \(\chi_{-2}(n) = 0\) for even \(n\). For a positive integer \(t\), let \(S(t) = \sum_{d \mid t} \chi_{-2}(d)\), the sum over the positive divisors \(d\) of \(t\). For every odd natural number \(m\), \(S(2m) = S(m)\).

public theorem divChiNeg2Sum_two_mul_of_odd {m : ℕ} (hodd : Odd m) :
    divChiNeg2Sum (2 * m) = divChiNeg2Sum m

Uses 3

Statement usesDivisor sum of the character \(\chi_{-2}\)

Proof usesMultiplicativity of the divisor sum of \(\chi_{-2}\) · The divisor sum of \(\chi_{-2}\) at powers of \(2\)

DefinitionRepresentations by \(x^2 + 2y^2\) as elements of \(\mathbb{Z}(\sqrt{-2})\)#✓fully proved

For every natural number \(j\), the map \((x, y) \mapsto x + y\sqrt{-2}\) is a bijection from the set of integer pairs \((x, y)\) with \(x^2 + 2y^2 = j\) to the set of elements \(z \in \mathbb{Z}[\sqrt{-2}]\) whose norm \(N(z)\) has absolute value \(j\).

public def pairEquivSqrtNegTwoNormFiber (j : ℕ) :
    {p : ℤ × ℤ // p.1 ^ 2 + 2 * p.2 ^ 2 = (j : ℤ)} ≃
      {z : ℤ√-2 // (Zsqrtd.norm z).natAbs = j} where
  toFun p := ⟨⟨p.1.1, p.1.2⟩, by
    rw [sqrtNegTwoNorm, p.2, Int.natAbs_natCast]⟩
  invFun z := ⟨(z.1.re, z.1.im), by
    have hnonneg : 0 ≤ Zsqrtd.norm z.1 := Zsqrtd.norm_nonneg (by norm_num) z.1
    have hnorm : Zsqrtd.norm z.1 = (j : ℤ) := by
      rw [← Int.natAbs_of_nonneg hnonneg, z.2]
    rwa [sqrtNegTwoNorm] at hnorm⟩
  left_inv p := Subtype.ext rfl
  right_inv z := Subtype.ext rfl

Used by 1

Used byNumber of representations by \(x^2 + 2y^2\)

TheoremNumber of representations by \(x^2 + 2y^2\)#✓fully proved

For every integer \(j \ge 1\), the number of pairs of integers \((x, y)\) with \(x^2 + 2y^2 = j\) equals \(2 \sum_{d \mid j} \chi(d)\), where \(d\) runs over the positive divisors of \(j\) and \(\chi\) is the Dirichlet character modulo \(8\) attached to \(\mathbb{Q}(\sqrt{-2})\): \(\chi(d) = 1\) if \(d \equiv 1, 3 \pmod 8\), \(\chi(d) = -1\) if \(d \equiv 5, 7 \pmod 8\), and \(\chi(d) = 0\) if \(d\) is even.

public theorem x2_add_two_sq_count (j : ℕ) (hj : 1 ≤ j) :
    (Fintype.card {p : ℤ × ℤ // p.1 ^ 2 + 2 * p.2 ^ 2 = (j : ℤ)} : ℤ) =
      2 * ∑ d ∈ j.divisors, ZMod.χ₈' d

Uses 4

Statement usesRepresentations by \(x^2 + 2y^2\) as elements of \(\mathbb{Z}(\sqrt{-2})\)

Proof usesDivisor sum of the character \(\chi_{-2}\) · Number of elements of \(\mathbb{Z}(\sqrt{-2})\) of a given norm · Elements of \(\mathbb{Z}(\sqrt{-2})\) of norm \(t\) counted by a divisor sum

18 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.