Sums of squares and representation numbers

Two-, three- and four-square theorems, Jacobi-type counts, Gaussian and Hurwitz integer methods, x²+2y² and similar representations.

• Geometric sums as sums of two squares
• Representation numbers of sums of squares
• Jacobi's two-square theorem
• Representations by squares and triangular numbers
• Representations by x² + 2y²
• Sums of four squares via Hurwitz continued fractions
• Sums of three squares
• Sums of two squares via the Stern–Brocot tree

TheoremLandau–Ramanujan theorem#✓fully proved

For real \(x\), let \(B(x)\) be the number of natural numbers \(m \le x\), including \(m = 0\), that can be written as \(m = a^2 + b^2\) with natural numbers \(a\) and \(b\). Then there is a constant \(c_0 > 0\) such that \(B(x)\) is asymptotically equivalent to \(c_0 x / \sqrt{\log x}\) as \(x \to \infty\).

This only asserts the existence of some positive constant \(c_0\); it does not identify \(c_0\) with the Landau–Ramanujan constant (the Euler product over the primes \(p \equiv 3 \pmod 4\) in the cited result). That identification is an intentional omission relative to the source.

public theorem landau_ramanujan_asymptotic :
    ∃ c₀ : ℝ, 0 < c₀ ∧
      Asymptotics.IsEquivalent (Filter.atTop : Filter ℝ)
        (fun x : ℝ =>
          ((Set.ncard {m : ℕ | (m : ℝ) ≤ x ∧ ∃ a b : ℕ, m = a ^ 2 + b ^ 2} : ℕ) : ℝ))
        (fun x : ℝ => c₀ * x / Real.sqrt (Real.log x))

Sources

• Labib Haddad and Charles Helou, "Representation of Integers by Near Quadratic Sequences," Journal of Integer Sequences 15 (2012), https://cs.uwaterloo.ca/journals/JIS/VOL15/Helou/helou3.tex, lines 483–486. Proof-method source (distinct from the statement source above): the proof adapts Wirsing's mean-value method as presented in Gérald Tenenbaum, Introduction to Analytic and Probabilistic Number Theory, Chapter III.4.

Uses 3

Proof usesMertens' theorem in arithmetic progressions · Chebyshev's function in a residue class · Prime number theorem for Chebyshev's function in a reduced residue class

TheoremPositive integers that are differences of two squares#✓fully proved

A positive natural number \(n\) can be written as \(n = a^2 - b^2\) with natural numbers \(a\) and \(b\) if and only if there is no natural number \(k\) with \(n = 4k + 2\).

theorem nat_eq_sq_sub_sq_iff_not_eq_four_mul_add_two
    (n : ℕ) (hn : 0 < n) :
    (∃ a b : ℕ, n = a ^ 2 - b ^ 2) ↔ ¬ ∃ k : ℕ, n = 4 * k + 2

Sources

• Arias, Borja, and Rubio cite D. M. Burton, "Elementary Number Theory," 7th edition, Theorem 13.4; truncated subtraction is exact on the witnesses.
• Fabián Arias, Jerson Borja, and Luis Rubio, "Counting Integers Representable as Images of Polynomials Modulo n," Journal of Integer Sequences 22 (2019), Article 19.6.7, Theorem, lines 821–823, https://cs.uwaterloo.ca/journals/JIS/VOL22/Borja/borja3.tex

TheoremSums of two coprime squares#✓fully proved

Let \(d > 2\) be a natural number. Then \(d = a^2 + b^2\) for some coprime positive natural numbers \(a\) and \(b\) if and only if there is a natural number \(q\), all of whose prime factors are congruent to \(1\) modulo \(4\), such that \(d = q\) or \(d = 2q\).

theorem sum_two_coprime_squares_characterization
    (d : ℕ) (hd : 2 < d) :
    ((∃ a b : ℕ, 0 < a ∧ 0 < b ∧ Nat.Coprime a b ∧ a ^ 2 + b ^ 2 = d) ↔
      ∃ q : ℕ, (∀ p ∈ q.primeFactors, p % 4 = 1) ∧ (d = q ∨ d = 2 * q))

Sources

• Nguyen Viet Dung and Luu Ba Thang, "The Number a²+b²−dc² Revisited", Journal of Integer Sequences 24 (2021), Article 21.9.3, theorem lines 105–107, https://cs.uwaterloo.ca/journals/JIS/VOL24/Thang/thang41.tex.

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.