Sums of powers of consecutive primes

TheoremCounting sums of a fixed number of consecutive prime powers#●ready to prove

Let \(p_1 < p_2 < \cdots\) be the primes. For natural numbers \(k > 1\), \(m > 0\) and \(x\), the number of integers \(n \le x\) of the form \(n = p_{\ell+1}^k + p_{\ell+2}^k + \cdots + p_{\ell+m}^k\) for some \(\ell \ge 0\) is at most \(\pi(\lfloor (x/m)^{1/k} \rfloor)\), the number of primes up to \((x/m)^{1/k}\).

public theorem_wanted card_consecutivePrimePowerSums_length_le (k m x : ℕ) (hk : 1 < k)
    (hm : 0 < m) :
    {n : ℕ | n ≤ x ∧ ∃ l, n = ∑ i ∈ range m, Nat.nth Nat.Prime (l + i) ^ k}.ncard ≤
      Nat.primeCounting ⌊((x : ℝ) / m) ^ ((1 : ℝ) / k)⌋₊

Sources

• Cathal O'Sullivan, Jonathan P. Sorenson, and Aryn Stahl, Algorithms and Bounds on the Sums of Powers of Consecutive Primes, INTEGERS 24 (2024), Article A4, Lemma 1 (quoted from [6]).

TheoremLength of the longest sum of consecutive prime powers#●ready to prove

Let \(p_1 < p_2 < \cdots\) be the primes, let \(k > 1\) be a natural number, and for a natural number \(x\) let \(M(x, k)\) be the largest \(m \le x\) with \(p_1^k + p_2^k + \cdots + p_m^k \le x\). Then \(M(x, k) \sim (k + 1)\, x^{1/(k+1)} / (\log x)^{k/(k+1)}\) (asymptotic equivalence) as \(x \to \infty\) through the natural numbers.

public theorem_wanted maxConsecutivePrimePowerSumLength_isEquivalent (k : ℕ) (hk : 1 < k) :
    (fun x : ℕ =>
        (Nat.findGreatest (fun m => ∑ i ∈ range m, Nat.nth Nat.Prime i ^ k ≤ x) x : ℝ)) ~[atTop]
      fun x : ℕ => (k + 1) * (x : ℝ) ^ ((1 : ℝ) / (k + 1)) /
        Real.log x ^ ((k : ℝ) / (k + 1))

Sources

• Cathal O'Sullivan, Jonathan P. Sorenson, and Aryn Stahl, Algorithms and Bounds on the Sums of Powers of Consecutive Primes, INTEGERS 24 (2024), Article A4, Lemma 2.

TheoremUpper bound for the number of sums of consecutive prime powers#●ready to prove

Let \(p_1 < p_2 < \cdots\) be the primes and let \(k > 1\) be a natural number. For a natural number \(x\) let \(s_k(x)\) be the number of pairs \((\ell, m)\) of integers with \(0 \le \ell < x\) and \(1 \le m \le x\) such that \(p_{\ell+1}^k + \cdots + p_{\ell+m}^k \le x\). Then for every real \(\varepsilon > 0\), for all sufficiently large \(x\), \(s_k(x) \le (1 + \varepsilon)\, c_k\, x^{2/(k+1)} / (\log x)^{2k/(k+1)}\), where \(c_k = \frac{k^2}{k-1} (k + 1)^{1 - 1/k}\).

public theorem_wanted card_consecutivePrimePowerSums_le (k : ℕ) (hk : 1 < k) (ε : ℝ)
    (hε : 0 < ε) :
    ∀ᶠ x : ℕ in atTop,
      (((range x ×ˢ Icc 1 x).filter (fun lm =>
          ∑ i ∈ range lm.2, Nat.nth Nat.Prime (lm.1 + i) ^ k ≤ x)).card : ℝ) ≤
        (1 + ε) * ((k ^ 2 / (k - 1) : ℝ) * ((k : ℝ) + 1) ^ (1 - (1 : ℝ) / k)) *
          ((x : ℝ) ^ ((2 : ℝ) / (k + 1)) / Real.log x ^ ((2 * k : ℝ) / (k + 1)))

Sources

• Cathal O'Sullivan, Jonathan P. Sorenson, and Aryn Stahl, Algorithms and Bounds on the Sums of Powers of Consecutive Primes, INTEGERS 24 (2024), Article A4, Theorem 1.

TheoremLower bound for the number of sums of consecutive prime powers#●ready to prove

Let \(p_1 < p_2 < \cdots\) be the primes and let \(k > 1\) be a natural number. For a natural number \(x\) let \(s_k(x)\) be the number of pairs \((\ell, m)\) of integers with \(0 \le \ell < x\) and \(1 \le m \le x\) such that \(p_{\ell+1}^k + \cdots + p_{\ell+m}^k \le x\), and let \(M(x, k)\) be the largest \(m \le x\) with \(p_1^k + \cdots + p_m^k \le x\). Then \(M(x, k)^2 / 2 \le s_k(x)\) for every \(x\), and for every real \(\varepsilon > 0\), for all sufficiently large \(x\), \((1 - \varepsilon) (k + 1)^2 x^{2/(k+1)} / \bigl(2 (\log x)^{2k/(k+1)}\bigr) \le M(x, k)^2 / 2\).

public theorem_wanted card_consecutivePrimePowerSums_ge (k : ℕ) (hk : 1 < k) :
    let s : ℕ → ℝ := fun x =>
      (((range x ×ˢ Icc 1 x).filter (fun lm =>
          ∑ i ∈ range lm.2, Nat.nth Nat.Prime (lm.1 + i) ^ k ≤ x)).card : ℝ)
    let M : ℕ → ℝ := fun x =>
      (Nat.findGreatest (fun m => ∑ i ∈ range m, Nat.nth Nat.Prime i ^ k ≤ x) x : ℝ)
    (∀ x : ℕ, M x ^ 2 / 2 ≤ s x) ∧
      ∀ ε : ℝ, 0 < ε → ∀ᶠ x : ℕ in atTop,
        (1 - ε) * (((k : ℝ) + 1) ^ 2 * (x : ℝ) ^ ((2 : ℝ) / (k + 1)) /
          (2 * Real.log x ^ ((2 * k : ℝ) / (k + 1)))) ≤ M x ^ 2 / 2

Sources

• Cathal O'Sullivan, Jonathan P. Sorenson, and Aryn Stahl, Algorithms and Bounds on the Sums of Powers of Consecutive Primes, INTEGERS 24 (2024), Article A4, Theorem 2.

TheoremUpper bound for the maximal gleeful chain length#●ready to prove

Let \(p_1 = 2, p_2 = 3, \dots\) be the primes in increasing order. Let \(k > 1\), \(M_0 \ge 6\), \(M \ge M_0\) and \(x\) be natural numbers with \(p_1^k + \cdots + p_M^k \le x < p_1^k + \cdots + p_{M+1}^k\). Put \(y = M_0\),

\[B = \frac{\log(y+1)}{\log y} + \frac{\log\log((y+1)^2)}{\log y} \cdot \frac{k}{k+1}\]

and \(C = (y/(y-1))^{1/(k+1)} B^{k/(k+1)}\), where \(\log\) is the natural logarithm. Then

\[M < 4^{1/(k+1)} \cdot \frac{(k+1)\, x^{1/(k+1)}}{(\log x)^{k/(k+1)}} \cdot C.\]

public theorem_wanted maxChainLength_lt (k M₀ M x : ℕ) (hk : 1 < k) (hM₀ : 6 ≤ M₀)
    (hM : M₀ ≤ M) (hx : ∑ i ∈ Finset.range M, Nat.nth Nat.Prime i ^ k ≤ x)
    (hx' : x < ∑ i ∈ Finset.range (M + 1), Nat.nth Nat.Prime i ^ k) :
    let y : ℝ := M₀
    let B := Real.log (y + 1) / Real.log y +
      Real.log (Real.log ((y + 1) ^ 2)) / Real.log y * ((k : ℝ) / (k + 1))
    let C := (y / (y - 1)) ^ ((1 : ℝ) / (k + 1)) * B ^ ((k : ℝ) / (k + 1))
    (M : ℝ) < (4 : ℝ) ^ ((1 : ℝ) / (k + 1)) *
      ((k + 1) * (x : ℝ) ^ ((1 : ℝ) / (k + 1)) / Real.log x ^ ((k : ℝ) / (k + 1))) * C

Sources

• Sara Moore and Jonathan P. Sorenson, Explicit Bounds and Parallel Algorithms for Counting Multiply Gleeful Numbers, INTEGERS 26 (2026), Article A84, Lemma 1, with B, C from Section 2.

TheoremLower bound for the maximal gleeful chain length#●ready to prove

Let \(p_1 = 2, p_2 = 3, \dots\) be the primes in increasing order. Let \(k > 1\), \(M_0 \ge 6\), \(M \ge M_0\) and \(x\) be natural numbers with \(p_1^k + \cdots + p_M^k \le x < p_1^k + \cdots + p_{M+1}^k\). Put \(y = M_0\) and

\[D = \frac{y}{y+3} \Big(\frac{\log(y/2)}{\log y + 2 \log\log(y+2)}\Big)^{k/(k+1)},\]

where \(\log\) is the natural logarithm. Then

\[\frac{(k+1)\, x^{1/(k+1)}}{(\log x)^{k/(k+1)}} \cdot D \le M.\]

public theorem_wanted le_maxChainLength (k M₀ M x : ℕ) (hk : 1 < k) (hM₀ : 6 ≤ M₀)
    (hM : M₀ ≤ M) (hx : ∑ i ∈ Finset.range M, Nat.nth Nat.Prime i ^ k ≤ x)
    (hx' : x < ∑ i ∈ Finset.range (M + 1), Nat.nth Nat.Prime i ^ k) :
    let y : ℝ := M₀
    let D := (y / (y + 3)) *
      (Real.log (y / 2) / (Real.log y + 2 * Real.log (Real.log (y + 2)))) ^
        ((k : ℝ) / (k + 1))
    (k + 1) * (x : ℝ) ^ ((1 : ℝ) / (k + 1)) / Real.log x ^ ((k : ℝ) / (k + 1)) * D ≤ M

Sources

• Sara Moore and Jonathan P. Sorenson, Explicit Bounds and Parallel Algorithms for Counting Multiply Gleeful Numbers, INTEGERS 26 (2026), Article A84, Lemma 2, with D from Section 2.

TheoremBounds for the logarithm of the maximal gleeful chain length#●ready to prove

Let \(p_1 = 2, p_2 = 3, \dots\) be the primes in increasing order. Let \(k > 1\), \(M_0 \ge 6\), \(M \ge M_0\) and \(x\) be natural numbers with \(p_1^k + \cdots + p_M^k \le x < p_1^k + \cdots + p_{M+1}^k\). Put \(y = M_0\), let \(\log\) be the natural logarithm, and set

\[A = \frac{\log(y/2)}{\log y},\]

\[B = \frac{\log(y+1)}{\log y} + \frac{\log\log((y+1)^2)}{\log y} \cdot \frac{k}{k+1}.\]

Then

\[\frac{\log x}{k+1} \cdot \frac{1}{B} \le \log M < \frac{\log x}{k+1} \cdot \frac{1}{A}.\]

public theorem_wanted log_maxChainLength_bounds (k M₀ M x : ℕ) (hk : 1 < k) (hM₀ : 6 ≤ M₀)
    (hM : M₀ ≤ M) (hx : ∑ i ∈ Finset.range M, Nat.nth Nat.Prime i ^ k ≤ x)
    (hx' : x < ∑ i ∈ Finset.range (M + 1), Nat.nth Nat.Prime i ^ k) :
    let y : ℝ := M₀
    let A := Real.log (y / 2) / Real.log y
    let B := Real.log (y + 1) / Real.log y +
      Real.log (Real.log ((y + 1) ^ 2)) / Real.log y * ((k : ℝ) / (k + 1))
    Real.log M < Real.log x / (k + 1) * (1 / A) ∧
      Real.log x / (k + 1) * (1 / B) ≤ Real.log M

Sources

• Sara Moore and Jonathan P. Sorenson, Explicit Bounds and Parallel Algorithms for Counting Multiply Gleeful Numbers, INTEGERS 26 (2026), Article A84, Lemma 3, with A, B from Section 2.

TheoremUpper bound for the number of gleeful representations#●ready to prove

Let \(p_1 = 2, p_2 = 3, \dots\) be the primes in increasing order, and for natural numbers \(k\) and \(x\) let \(s_k(x)\) be the number of pairs \((n, m)\) of natural numbers with \(m \ge 1\) and \(p_{n+1}^k + \cdots + p_{n+m}^k \le x\). Let \(k > 1\), \(M_0 \ge 6\) and \(x\) be natural numbers with \(p_1^k + \cdots + p_{M_0}^k \le x\). Put \(y = M_0\), let \(\log\) be the natural logarithm, and set

\[A = \frac{\log(y/2)}{\log y},\]

\[B = \frac{\log(y+1)}{\log y} + \frac{\log\log((y+1)^2)}{\log y} \cdot \frac{k}{k+1},\]

\[C = \Big(\frac{y}{y-1}\Big)^{1/(k+1)} B^{k/(k+1)}, \qquad E = 1 + \frac{1}{(k+1)A - 1},\]

\[F = \Big(\frac{y+1}{y}\Big)^{(k-1)/k} 4^{(k-1)/(k(k+1))} C^{(k-1)/k} E,\]

\(U = 1.25506\,F\) and \(c_k = \frac{k^2}{k-1} (k+1)^{(k-1)/k}\). Then

\[s_k(x) \le c_k \cdot \frac{x^{2/(k+1)}}{(\log x)^{2k/(k+1)}} \cdot U.\]

The paper prints the exponent of \(\log x\) as \(k/(k+1)\); its proof ends with \(2k/(k+1)\), which is stated here and implies the printed bound because \(\log x \ge 1\).

MetaMathlibExt.gleefulRepCount_le · 16 lines

public theorem_wanted gleefulRepCount_le (k M₀ x : ℕ) (hk : 1 < k) (hM₀ : 6 ≤ M₀)
    (hx : ∑ i ∈ Finset.range M₀, Nat.nth Nat.Prime i ^ k ≤ x) :
    let y : ℝ := M₀
    let κ : ℝ := k
    let A := Real.log (y / 2) / Real.log y
    let B := Real.log (y + 1) / Real.log y +
      Real.log (Real.log ((y + 1) ^ 2)) / Real.log y * (κ / (κ + 1))
    let C := (y / (y - 1)) ^ (1 / (κ + 1)) * B ^ (κ / (κ + 1))
    let E := 1 + 1 / ((κ + 1) * A - 1)
    let F := ((y + 1) / y) ^ ((κ - 1) / κ) * (4 : ℝ) ^ ((κ - 1) / (κ * (κ + 1))) *
      C ^ ((κ - 1) / κ) * E
    let U := 1.25506 * F
    let c := κ ^ 2 / (κ - 1) * (κ + 1) ^ ((κ - 1) / κ)
    ({q : ℕ × ℕ | 0 < q.2 ∧
        ∑ i ∈ Finset.range q.2, Nat.nth Nat.Prime (q.1 + i) ^ k ≤ x}.ncard : ℝ) ≤
      c * ((x : ℝ) ^ (2 / (κ + 1)) / Real.log x ^ (2 * κ / (κ + 1))) * U

Sources

• Sara Moore and Jonathan P. Sorenson, Explicit Bounds and Parallel Algorithms for Counting Multiply Gleeful Numbers, INTEGERS 26 (2026), Article A84, Theorem 1 and its proof, with c_k, A, B, C, E, F, U from Section 2.

TheoremLower bound for the number of gleeful representations#●ready to prove

Let \(p_1 = 2, p_2 = 3, \dots\) be the primes in increasing order, and for natural numbers \(k\) and \(x\) let \(s_k(x)\) be the number of pairs \((n, m)\) of natural numbers with \(m \ge 1\) and \(p_{n+1}^k + \cdots + p_{n+m}^k \le x\). Let \(k > 1\), \(M_0 \ge 6\) and \(x\) be natural numbers with \(p_1^k + \cdots + p_{M_0}^k \le x\). Put \(y = M_0\), let \(\log\) be the natural logarithm, and set

\[D = \frac{y}{y+3} \Big(\frac{\log(y/2)}{\log y + 2 \log\log(y+2)}\Big)^{k/(k+1)}\]

and \(L = \frac{y-1}{y} D^2\). Then

\[\frac{(k+1)^2}{2} \cdot \frac{x^{2/(k+1)}}{(\log x)^{2k/(k+1)}} \cdot L \le s_k(x).\]

The paper prints the exponent of \(\log x\) as \(k/(k+1)\); its proof gives \(2k/(k+1)\), which is stated here. The printed form contradicts the upper bound for \(s_k(x)\) for large \(x\).

public theorem_wanted le_gleefulRepCount (k M₀ x : ℕ) (hk : 1 < k) (hM₀ : 6 ≤ M₀)
    (hx : ∑ i ∈ Finset.range M₀, Nat.nth Nat.Prime i ^ k ≤ x) :
    let y : ℝ := M₀
    let κ : ℝ := k
    let D := (y / (y + 3)) *
      (Real.log (y / 2) / (Real.log y + 2 * Real.log (Real.log (y + 2)))) ^ (κ / (κ + 1))
    let L := (y - 1) / y * D ^ 2
    (κ + 1) ^ 2 / 2 * ((x : ℝ) ^ (2 / (κ + 1)) / Real.log x ^ (2 * κ / (κ + 1))) * L ≤
      ({q : ℕ × ℕ | 0 < q.2 ∧
        ∑ i ∈ Finset.range q.2, Nat.nth Nat.Prime (q.1 + i) ^ k ≤ x}.ncard : ℝ)

Sources

• Sara Moore and Jonathan P. Sorenson, Explicit Bounds and Parallel Algorithms for Counting Multiply Gleeful Numbers, INTEGERS 26 (2026), Article A84, Theorem 2 and its proof, with D, L from Section 2.

9 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.