Dirichlet convolutions of digit sums

DefinitionDigit-sum arithmetic function#✓fully proved

For a natural number \(q\), \(s_q\) is the arithmetic function that sends \(n\) to \(s_q(n)\), the sum of the digits of \(n\) in base \(q\). Its \(k\)-th Dirichlet power is the \(k\)-fold Dirichlet convolution \(s_q^{(k)}\), so \(s_q^{(1)} = s_q\) and \(s_q^{(k)} = s_q * s_q^{(k-1)}\) for \(k \ge 2\).

For \(q \le 1\) the base-\(q\) digit expansion is degenerate and \(s_q(n) = n\).

def digitSumArith (q : ℕ) : ArithmeticFunction ℕ :=
  ⟨fun n => (Nat.digits q n).sum, by simp⟩

Sources

• Ka Lun Wong and Erdenebileg Erdenebat, Asymptotics of Partial Sums of Dirichlet Convolutions of Digital Sum Functions in Arbitrary Bases, INTEGERS 26 (2026), Article A43, Section 1 (definition of s_q and of s_q^{(k)}).

Used by 4

Used byValue of the digit-sum arithmetic function · Partial sums of the iterated digit-sum convolutions · The second digit-sum convolution · Partial sums of the second digit-sum convolution

TheoremValue of the digit-sum arithmetic function#✓fully proved

For natural numbers \(q\) and \(n\), the base-\(q\) digit-sum arithmetic function \(s_q\) takes at \(n\) the value \(s_q(n)\), the sum of the digits of \(n\) in base \(q\).

theorem digitSumArith_apply (q n : ℕ) : digitSumArith q n = (Nat.digits q n).sum

Sources

• Ka Lun Wong and Erdenebileg Erdenebat, Asymptotics of Partial Sums of Dirichlet Convolutions of Digital Sum Functions in Arbitrary Bases, INTEGERS 26 (2026), Article A43, Section 1.

Uses 1

Statement usesDigit-sum arithmetic function

TheoremThe second digit-sum convolution#✓fully proved

For natural numbers \(q\) and \(n\), the Dirichlet square \(s_q^{(2)} = s_q * s_q\) of the base-\(q\) digit-sum function \(s_q\) satisfies \(s_q^{(2)}(n) = \sum_{de = n} s_q(d) \, s_q(e)\), where the sum runs over the pairs \((d, e)\) of positive integers with \(de = n\) (there are none for \(n = 0\), and then both sides are \(0\)).

theorem digitSumArith_sq_apply (q n : ℕ) :
    (digitSumArith q ^ 2) n =
      ∑ x ∈ n.divisorsAntidiagonal, (Nat.digits q x.1).sum * (Nat.digits q x.2).sum

Sources

• Ka Lun Wong and Erdenebileg Erdenebat, Asymptotics of Partial Sums of Dirichlet Convolutions of Digital Sum Functions in Arbitrary Bases, INTEGERS 26 (2026), Article A43, Section 1 (definition of s_q^{(2)}).

Uses 1

Statement usesDigit-sum arithmetic function

DefinitionDelange's function#✓fully proved

For a natural number \(q\), Delange's function in base \(q\) is the function of a real number \(x\) given by \(g(x) = \int_0^x \left(\lfloor q t \rfloor - q \lfloor t \rfloor - \frac{q - 1}{2}\right) dt\), where \(\lfloor \cdot \rfloor\) is the floor function.

noncomputable def trollopeDelangeIntegral (q : ℕ) (x : ℝ) : ℝ :=
  ∫ t in (0 : ℝ)..x, ((⌊(q : ℝ) * t⌋ : ℝ) - q * ⌊t⌋ - ((q : ℝ) - 1) / 2)

Sources

• Ka Lun Wong and Erdenebileg Erdenebat, Asymptotics of Partial Sums of Dirichlet Convolutions of Digital Sum Functions in Arbitrary Bases, INTEGERS 26 (2026), Article A43, Theorem 1 (definition of g).

Used by 4

Used byDelange's function is eventually bounded · Delange's function vanishes at zero · Delange's series · Delange's series vanishes at zero

TheoremDelange's function vanishes at zero#✓fully proved

For every natural number \(q\), Delange's function \(g\) in base \(q\) satisfies \(g(0) = 0\).

theorem trollopeDelangeIntegral_zero (q : ℕ) : trollopeDelangeIntegral q 0 = 0

Sources

• Ka Lun Wong and Erdenebileg Erdenebat, Asymptotics of Partial Sums of Dirichlet Convolutions of Digital Sum Functions in Arbitrary Bases, INTEGERS 26 (2026), Article A43, Theorem 1.

Uses 1 · Used by 1

Statement usesDelange's function

Used byDelange's series vanishes at zero

DefinitionDelange's series#✓fully proved

For a natural number \(q\), let \(g\) be Delange's function in base \(q\). Delange's series in base \(q\) is the function of a real number \(x\) given by \(h(x) = \sum_{r \ge 0} g(q^r x)/q^r\), where the sum is taken to be \(0\) when the series is not summable.

noncomputable def trollopeDelangeSeries (q : ℕ) (x : ℝ) : ℝ :=
  ∑' r : ℕ, trollopeDelangeIntegral q ((q : ℝ) ^ r * x) / (q : ℝ) ^ r

Sources

• Ka Lun Wong and Erdenebileg Erdenebat, Asymptotics of Partial Sums of Dirichlet Convolutions of Digital Sum Functions in Arbitrary Bases, INTEGERS 26 (2026), Article A43, Theorem 1 (definition of h).

Uses 1 · Used by 7

Statement usesDelange's function

Used bySize bounds for the Trollope–Delange auxiliary functions · Trollope–Delange formula for real \(x\) · Trollope–Delange remainder · The Trollope–Delange remainder vanishes at zero · Trollope–Delange fluctuation · Periodicity of the Trollope–Delange fluctuation · Delange's series vanishes at zero

TheoremDelange's series vanishes at zero#✓fully proved

For every natural number \(q\), Delange's series \(h\) in base \(q\) satisfies \(h(0) = 0\).

theorem trollopeDelangeSeries_zero (q : ℕ) : trollopeDelangeSeries q 0 = 0

Sources

• Ka Lun Wong and Erdenebileg Erdenebat, Asymptotics of Partial Sums of Dirichlet Convolutions of Digital Sum Functions in Arbitrary Bases, INTEGERS 26 (2026), Article A43, Theorem 1.

Uses 3 · Used by 1

Statement usesDelange's series

Proof usesDelange's function · Delange's function vanishes at zero

Used byThe Trollope–Delange remainder vanishes at zero

DefinitionTrollope–Delange fluctuation#✓fully proved

Let \(q\) be a natural number and let \(h\) be Delange's series in base \(q\). The Trollope–Delange fluctuation in base \(q\) is the function of a real number \(x\) given by \(F(x) = \frac{q - 1}{2}(1 + \lfloor x \rfloor - x) + q^{1 + \lfloor x \rfloor - x}\, h(q^{x - \lfloor x \rfloor - 1})\), where \(\lfloor x \rfloor\) is the floor of \(x\).

noncomputable def trollopeDelangeFluctuation (q : ℕ) (x : ℝ) : ℝ :=
  ((q : ℝ) - 1) / 2 * (1 + ⌊x⌋ - x) +
    (q : ℝ) ^ (1 + ⌊x⌋ - x) * trollopeDelangeSeries q ((q : ℝ) ^ (x - ⌊x⌋ - 1))

Sources

• Ka Lun Wong and Erdenebileg Erdenebat, Asymptotics of Partial Sums of Dirichlet Convolutions of Digital Sum Functions in Arbitrary Bases, INTEGERS 26 (2026), Article A43, Theorem 1 (definition of F).

Uses 1 · Used by 9

Statement usesDelange's series

Used bySize bounds for the Trollope–Delange auxiliary functions · Double integral of the Trollope–Delange fluctuation · The double fluctuation integral vanishes at 1 · Integral of the Trollope–Delange fluctuation · The fluctuation integral vanishes at \(1\) · Trollope–Delange formula for real \(x\) · Bound for a weighted sum of the fluctuation · Exact formulas for the reciprocal digit sums · Periodicity of the Trollope–Delange fluctuation

TheoremPeriodicity of the Trollope–Delange fluctuation#✓fully proved

For every natural number \(q\) and every real number \(x\), the Trollope–Delange fluctuation \(F\) in base \(q\) satisfies \(F(x + 1) = F(x)\).

theorem trollopeDelangeFluctuation_add_one (q : ℕ) (x : ℝ) :
    trollopeDelangeFluctuation q (x + 1) = trollopeDelangeFluctuation q x

Sources

• Ka Lun Wong and Erdenebileg Erdenebat, Asymptotics of Partial Sums of Dirichlet Convolutions of Digital Sum Functions in Arbitrary Bases, INTEGERS 26 (2026), Article A43, Theorem 1 (F is 1-periodic).

Uses 2

Statement usesTrollope–Delange fluctuation

Proof usesDelange's series

DefinitionTrollope–Delange remainder#✓fully proved

Let \(q\) be a natural number, write \(s_q(n)\) for the sum of the base-\(q\) digits of a natural number \(n\) (with \(s_q(n) = n\) when \(q \le 1\)), and let \(h\) be Delange's series in base \(q\). For a real number \(x\), let \(n_x\) be the floor of \(x\) when \(x \ge 0\) and \(n_x = 0\) when \(x < 0\). The remainder of the Trollope–Delange formula is \(J(x) = (1 + n_x - x)\, s_q(n_x) - h(x)\).

noncomputable def digitSumRemainder (q : ℕ) (x : ℝ) : ℝ :=
  (1 + ⌊x⌋₊ - x) * ((Nat.digits q ⌊x⌋₊).sum : ℝ) - trollopeDelangeSeries q x

Sources

• Ka Lun Wong and Erdenebileg Erdenebat, Asymptotics of Partial Sums of Dirichlet Convolutions of Digital Sum Functions in Arbitrary Bases, INTEGERS 26 (2026), Article A43, Lemma 1 (definition of J).

Uses 1 · Used by 7

Statement usesDelange's series

Used bySize bounds for the Trollope–Delange auxiliary functions · Exact formulas for the reciprocal digit sums · Double integral of the Trollope–Delange remainder · The double remainder integral vanishes at \(1\) · Weighted integral of the Trollope–Delange remainder · The remainder integral vanishes at \(1\) · The Trollope–Delange remainder vanishes at zero

TheoremThe Trollope–Delange remainder vanishes at zero#✓fully proved

For every natural number \(q\), the remainder \(J\) of the Trollope–Delange formula in base \(q\) satisfies \(J(0) = 0\).

theorem digitSumRemainder_zero (q : ℕ) : digitSumRemainder q 0 = 0

Sources

• Ka Lun Wong and Erdenebileg Erdenebat, Asymptotics of Partial Sums of Dirichlet Convolutions of Digital Sum Functions in Arbitrary Bases, INTEGERS 26 (2026), Article A43, Lemma 1.

Uses 3

Statement usesTrollope–Delange remainder

Proof usesDelange's series · Delange's series vanishes at zero

DefinitionIntegral of the Trollope–Delange fluctuation#✓fully proved

For a natural number \(q\) and a real number \(x\), let \(F\) be the Trollope–Delange fluctuation in base \(q\). Then \(G(x)\) is the real number

\[G(x) = \int_1^x \frac{F(\log u / \log q)}{u} \, du,\]

where the integral is oriented, so that \(\int_1^x = -\int_x^1\) when \(x < 1\).

noncomputable def digitSumFluctuationIntegral (q : ℕ) (x : ℝ) : ℝ :=
  ∫ u in (1 : ℝ)..x, trollopeDelangeFluctuation q (log u / log q) / u

Sources

• Ka Lun Wong and Erdenebileg Erdenebat, Asymptotics of Partial Sums of Dirichlet Convolutions of Digital Sum Functions in Arbitrary Bases, INTEGERS 26 (2026), Article A43, Lemma 1 (definition of G).

Uses 1 · Used by 3

Statement usesTrollope–Delange fluctuation

Used bySize bounds for the Trollope–Delange auxiliary functions · The fluctuation integral vanishes at \(1\) · Exact formulas for the reciprocal digit sums

TheoremThe fluctuation integral vanishes at \(1\)#✓fully proved

For every natural number \(q\), let \(F\) be the Trollope–Delange fluctuation in base \(q\) and \(G(x) = \int_1^x F(\log u / \log q) \, du / u\). Then \(G(1) = 0\).

theorem digitSumFluctuationIntegral_one (q : ℕ) : digitSumFluctuationIntegral q 1 = 0

Sources

• Ka Lun Wong and Erdenebileg Erdenebat, Asymptotics of Partial Sums of Dirichlet Convolutions of Digital Sum Functions in Arbitrary Bases, INTEGERS 26 (2026), Article A43, Lemma 1.

Uses 2

Statement usesIntegral of the Trollope–Delange fluctuation

Proof usesTrollope–Delange fluctuation

DefinitionDouble integral of the Trollope–Delange fluctuation#✓fully proved

For a natural number \(q\) and a real number \(x\), let \(F\) be the Trollope–Delange fluctuation in base \(q\). Then \(H(x)\) is the real number

\[H(x) = \int_1^x \frac{1}{u} \left( \int_1^u \frac{F(\log v / \log q)}{v} \, dv \right) du,\]

where the integrals are oriented, so that \(\int_a^b = -\int_b^a\) when \(b < a\).

noncomputable def digitSumFluctuationDoubleIntegral (q : ℕ) (x : ℝ) : ℝ :=
  ∫ u in (1 : ℝ)..x, (∫ v in (1 : ℝ)..u, trollopeDelangeFluctuation q (log v / log q) / v) / u

Sources

• Ka Lun Wong and Erdenebileg Erdenebat, Asymptotics of Partial Sums of Dirichlet Convolutions of Digital Sum Functions in Arbitrary Bases, INTEGERS 26 (2026), Article A43, Lemma 1 (definition of H).

Uses 1 · Used by 3

Statement usesTrollope–Delange fluctuation

Used bySize bounds for the Trollope–Delange auxiliary functions · The double fluctuation integral vanishes at 1 · Exact formulas for the reciprocal digit sums

TheoremThe double fluctuation integral vanishes at 1#✓fully proved

For every natural number \(q\), the double integral \(H(x) = \int_1^x \int_1^u F(\log v / \log q) \, dv/v \, du/u\) of the Trollope–Delange fluctuation \(F\) for base \(q\) satisfies \(H(1) = 0\).

theorem digitSumFluctuationDoubleIntegral_one (q : ℕ) :
    digitSumFluctuationDoubleIntegral q 1 = 0

Sources

• Ka Lun Wong and Erdenebileg Erdenebat, Asymptotics of Partial Sums of Dirichlet Convolutions of Digital Sum Functions in Arbitrary Bases, INTEGERS 26 (2026), Article A43, Lemma 1.

Uses 2

Statement usesDouble integral of the Trollope–Delange fluctuation

Proof usesTrollope–Delange fluctuation

DefinitionWeighted integral of the Trollope–Delange remainder#✓fully proved

For a natural number \(q\), let \(J\) be the remainder of the Trollope–Delange formula in base \(q\). For a real number \(x\), define \(K(x) = \int_1^x J(u)/u^2 \, du\), an oriented interval integral (so \(K(x) = -\int_x^1 J(u)/u^2 \, du\) when \(x < 1\)) that is taken to be \(0\) when \(J(u)/u^2\) is not integrable on the interval between \(1\) and \(x\).

noncomputable def digitSumRemainderIntegral (q : ℕ) (x : ℝ) : ℝ :=
  ∫ u in (1 : ℝ)..x, digitSumRemainder q u / u ^ 2

Sources

• Ka Lun Wong and Erdenebileg Erdenebat, Asymptotics of Partial Sums of Dirichlet Convolutions of Digital Sum Functions in Arbitrary Bases, INTEGERS 26 (2026), Article A43, Lemma 1 (definition of K).

Uses 1 · Used by 3

Statement usesTrollope–Delange remainder

Used bySize bounds for the Trollope–Delange auxiliary functions · Exact formulas for the reciprocal digit sums · The remainder integral vanishes at \(1\)

TheoremThe remainder integral vanishes at \(1\)#✓fully proved

For every natural number \(q\), let \(J\) be the remainder of the Trollope–Delange formula in base \(q\) and \(K(x) = \int_1^x J(u) \, du / u^2\). Then \(K(1) = 0\).

theorem digitSumRemainderIntegral_one (q : ℕ) : digitSumRemainderIntegral q 1 = 0

Sources

• Ka Lun Wong and Erdenebileg Erdenebat, Asymptotics of Partial Sums of Dirichlet Convolutions of Digital Sum Functions in Arbitrary Bases, INTEGERS 26 (2026), Article A43, Lemma 1.

Uses 2

Statement usesWeighted integral of the Trollope–Delange remainder

Proof usesTrollope–Delange remainder

DefinitionDouble integral of the Trollope–Delange remainder#✓fully proved

For a natural number \(q\) and a real number \(x\), let \(J\) be the remainder of the Trollope–Delange formula in base \(q\). Then \(L(x)\) is the real number

\[L(x) = \int_1^x \frac{1}{u} \left( \int_1^u \frac{J(v)}{v^2} \, dv \right) du,\]

where the integrals are oriented, so that \(\int_a^b = -\int_b^a\) when \(b < a\).

noncomputable def digitSumRemainderDoubleIntegral (q : ℕ) (x : ℝ) : ℝ :=
  ∫ u in (1 : ℝ)..x, (∫ v in (1 : ℝ)..u, digitSumRemainder q v / v ^ 2) / u

Sources

• Ka Lun Wong and Erdenebileg Erdenebat, Asymptotics of Partial Sums of Dirichlet Convolutions of Digital Sum Functions in Arbitrary Bases, INTEGERS 26 (2026), Article A43, Lemma 1 (definition of L).

Uses 1 · Used by 3

Statement usesTrollope–Delange remainder

Used bySize bounds for the Trollope–Delange auxiliary functions · Exact formulas for the reciprocal digit sums · The double remainder integral vanishes at \(1\)

TheoremThe double remainder integral vanishes at \(1\)#✓fully proved

For every natural number \(q\), let \(J\) be the remainder of the Trollope–Delange formula in base \(q\) and \(L(x) = \int_1^x \frac{1}{u} \int_1^u \frac{J(v)}{v^2} \, dv \, du\). Then \(L(1) = 0\).

theorem digitSumRemainderDoubleIntegral_one (q : ℕ) :
    digitSumRemainderDoubleIntegral q 1 = 0

Sources

• Ka Lun Wong and Erdenebileg Erdenebat, Asymptotics of Partial Sums of Dirichlet Convolutions of Digital Sum Functions in Arbitrary Bases, INTEGERS 26 (2026), Article A43, Lemma 1.

Uses 2

Statement usesDouble integral of the Trollope–Delange remainder

Proof usesTrollope–Delange remainder

DefinitionDigit-convolution coefficients#✓fully proved

For a natural number \(q\), the base-\(q\) digit-convolution coefficients are the real numbers \(a(k)\), \(k \ge 0\), given by \(a(0) = a(1) = 0\), \(a(2) = \frac{(q - 1)^2}{24 \log^2 q}\) and, for every \(k \ge 3\),

\[a(k) = a(k - 1) \cdot \frac{q - 1}{2 \log q} \sum_{j=0}^{2k-3} \binom{2k-3}{j} \frac{(-1)^j}{j + 2},\]

where \(\log\) is the natural logarithm and division by \(0\) is read as \(0\) (this matters only for \(q \le 1\)). The values \(a(0)\) and \(a(1)\) are placeholders; only \(a(k)\) with \(k \ge 2\) is used.

noncomputable def digitConvolutionCoeff (q : ℕ) : ℕ → ℝ
  | 0 => 0
  | 1 => 0
  | 2 => ((q : ℝ) - 1) ^ 2 / (24 * log q ^ 2)
  | k + 3 =>
    digitConvolutionCoeff q (k + 2) * (((q : ℝ) - 1) / (2 * log q)) *
      ∑ j ∈ Finset.range (2 * (k + 3) - 3 + 1),
        ((2 * (k + 3) - 3).choose j : ℝ) * (-1) ^ j / ((j : ℝ) + 2)

Sources

• Ka Lun Wong and Erdenebileg Erdenebat, Asymptotics of Partial Sums of Dirichlet Convolutions of Digital Sum Functions in Arbitrary Bases, INTEGERS 26 (2026), Article A43, Theorem 3 (definition of a(k)).

Used by 3

Used byRecurrence for the digit-convolution coefficients · Second digit-convolution coefficient · Partial sums of the iterated digit-sum convolutions

TheoremSecond digit-convolution coefficient#✓fully proved

For every natural number \(q\), the base-\(q\) digit-convolution coefficient \(a(2)\) equals \(\frac{(q - 1)^2}{24 \log^2 q}\), with division by \(0\) read as \(0\) (this matters only for \(q \le 1\)).

theorem digitConvolutionCoeff_two (q : ℕ) :
    digitConvolutionCoeff q 2 = ((q : ℝ) - 1) ^ 2 / (24 * log q ^ 2)

Sources

• Ka Lun Wong and Erdenebileg Erdenebat, Asymptotics of Partial Sums of Dirichlet Convolutions of Digital Sum Functions in Arbitrary Bases, INTEGERS 26 (2026), Article A43, Theorem 3.

Uses 1

Statement usesDigit-convolution coefficients

TheoremRecurrence for the digit-convolution coefficients#✓fully proved

For every natural number \(q\) and every integer \(k \ge 2\), the base-\(q\) digit-convolution coefficients \(a(k)\) satisfy

\[a(k + 1) = a(k) \cdot \frac{q - 1}{2 \log q} \sum_{j=0}^{2k-1} \binom{2k-1}{j} \frac{(-1)^j}{j + 2},\]

where division by \(0\) is read as \(0\) (this matters only for \(q \le 1\)).

theorem digitConvolutionCoeff_succ (q : ℕ) {k : ℕ} (hk : 2 ≤ k) :
    digitConvolutionCoeff q (k + 1) =
      digitConvolutionCoeff q k * (((q : ℝ) - 1) / (2 * log q)) *
        ∑ j ∈ Finset.range (2 * (k + 1) - 3 + 1),
          ((2 * (k + 1) - 3).choose j : ℝ) * (-1) ^ j / ((j : ℝ) + 2)

Sources

• Ka Lun Wong and Erdenebileg Erdenebat, Asymptotics of Partial Sums of Dirichlet Convolutions of Digital Sum Functions in Arbitrary Bases, INTEGERS 26 (2026), Article A43, Theorem 3.

Uses 1

Statement usesDigit-convolution coefficients

TheoremTrollope–Delange formula for real \(x\)#●ready to prove

Let \(q \ge 2\) be an integer, let \(s_q(n)\) denote the sum of the base-\(q\) digits of \(n\), and let \(F\) be the Trollope–Delange fluctuation and \(h\) Delange's series in base \(q\). For every real number \(x \ge 1\),

\[\sum_{n=1}^{\lfloor x \rfloor} s_q(n) = \frac{q - 1}{2 \log q} \, x \log x + x F\left(\frac{\log x}{\log q}\right) - h(x) + (1 + \lfloor x \rfloor - x) \, s_q(\lfloor x \rfloor).\]

public theorem_wanted digitSum_partialSum_trollopeDelange (q : ℕ) (hq : 2 ≤ q) (x : ℝ)
    (hx : 1 ≤ x) :
    ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, ((Nat.digits q n).sum : ℝ) =
      ((q : ℝ) - 1) / (2 * log q) * x * log x +
        x * trollopeDelangeFluctuation q (log x / log q) - trollopeDelangeSeries q x +
          (1 + ⌊x⌋₊ - x) * ((Nat.digits q ⌊x⌋₊).sum : ℝ)

Sources

• Ka Lun Wong and Erdenebileg Erdenebat, Asymptotics of Partial Sums of Dirichlet Convolutions of Digital Sum Functions in Arbitrary Bases, INTEGERS 26 (2026), Article A43, Theorem 1, equation (1).

Uses 2

Statement usesTrollope–Delange fluctuation · Delange's series

TheoremDelange's function is eventually bounded#●ready to prove

For every natural number \(q \ge 2\), Delange's function \(g\) in base \(q\) satisfies \(g(x) = O(1)\) as \(x \to +\infty\).

public theorem_wanted trollopeDelangeIntegral_isBigO_one (q : ℕ) (hq : 2 ≤ q) :
    trollopeDelangeIntegral q =O[atTop] (fun _ => (1 : ℝ))

Sources

• Ka Lun Wong and Erdenebileg Erdenebat, Asymptotics of Partial Sums of Dirichlet Convolutions of Digital Sum Functions in Arbitrary Bases, INTEGERS 26 (2026), Article A43, Lemma 2.

Uses 1

Statement usesDelange's function

TheoremExact formulas for the reciprocal digit sums#●ready to prove

Let \(q \ge 2\) be an integer and let \(s_q(n)\) denote the sum of the base-\(q\) digits of \(n\). Let \(F\) be the Trollope–Delange fluctuation and \(J\) the remainder of the Trollope–Delange formula in base \(q\), and for real \(x\) put \(G(x) = \int_1^x F(\log u / \log q) \, du / u\), \(H(x) = \int_1^x G(u) \, du / u\), \(K(x) = \int_1^x J(u) \, du / u^2\) and \(L(x) = \int_1^x K(u) \, du / u\). Then for every real number \(x \ge 1\),

\[\sum_{n=1}^{\lfloor x \rfloor} \frac{s_q(n)}{n} = \frac{(q - 1) \log^2 x}{4 \log q} + \frac{(q - 1) \log x}{2 \log q} + F\left(\frac{\log x}{\log q}\right) + G(x) + \frac{J(x)}{x} + K(x)\]

and

\[\sum_{n=1}^{\lfloor x \rfloor} \frac{s_q(n) \log n}{n} = \frac{(q - 1) \log^3 x}{6 \log q} + \frac{(q - 1) \log^2 x}{4 \log q} + \log x \cdot F\left(\frac{\log x}{\log q}\right) + (\log x - 1) \, G(x) - H(x) + \frac{J(x) \log x}{x} + (\log x - 1) \, K(x) - L(x).\]

public theorem_wanted digitSum_reciprocal_sums_eq (q : ℕ) (hq : 2 ≤ q) (x : ℝ) (hx : 1 ≤ x) :
    ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, ((Nat.digits q n).sum : ℝ) / n =
        ((q : ℝ) - 1) * log x ^ 2 / (4 * log q) + ((q : ℝ) - 1) * log x / (2 * log q) +
          trollopeDelangeFluctuation q (log x / log q) + digitSumFluctuationIntegral q x +
          digitSumRemainder q x / x + digitSumRemainderIntegral q x ∧
      ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, ((Nat.digits q n).sum : ℝ) * log n / n =
        ((q : ℝ) - 1) * log x ^ 3 / (6 * log q) + ((q : ℝ) - 1) * log x ^ 2 / (4 * log q) +
          log x * trollopeDelangeFluctuation q (log x / log q) +
          (log x - 1) * digitSumFluctuationIntegral q x -
          digitSumFluctuationDoubleIntegral q x + digitSumRemainder q x * log x / x +
          (log x - 1) * digitSumRemainderIntegral q x - digitSumRemainderDoubleIntegral q x

Sources

• Ka Lun Wong and Erdenebileg Erdenebat, Asymptotics of Partial Sums of Dirichlet Convolutions of Digital Sum Functions in Arbitrary Bases, INTEGERS 26 (2026), Article A43, Lemma 1, equations (4) and (5).

Uses 6

Statement usesDouble integral of the Trollope–Delange fluctuation · Integral of the Trollope–Delange fluctuation · Trollope–Delange remainder · Double integral of the Trollope–Delange remainder · Weighted integral of the Trollope–Delange remainder · Trollope–Delange fluctuation

TheoremSize bounds for the Trollope–Delange auxiliary functions#●ready to prove

Let \(q \ge 2\) be an integer. For base \(q\), let \(h\) be Delange's series, \(F\) the Trollope–Delange fluctuation, \(J\) the remainder of the Trollope–Delange formula, and \(G(x) = \int_1^x F(\log u / \log q) \, du/u\), \(H(x) = \int_1^x \int_1^u F(\log v / \log q) \, dv/v \, du/u\), \(K(x) = \int_1^x J(u) \, du/u^2\) and \(L(x) = \int_1^x \int_1^u J(v) \, dv/v^2 \, du/u\). Then \(F\) is bounded on \(\mathbb{R}\), and as \(x \to \infty\) through the reals, \(h(x) = O(1)\), \(J(x) = O(\log x)\), \(G(x) = O(\log x)\), \(H(x) = O(\log^2 x)\), \(K(x) = O(1)\) and \(L(x) = O(\log x)\).

public theorem_wanted digitSum_auxiliary_isBigO (q : ℕ) (hq : 2 ≤ q) :
    trollopeDelangeSeries q =O[atTop] (fun _ => (1 : ℝ)) ∧
      (∃ C : ℝ, ∀ x : ℝ, |trollopeDelangeFluctuation q x| ≤ C) ∧
      digitSumRemainder q =O[atTop] log ∧
      digitSumFluctuationIntegral q =O[atTop] log ∧
      digitSumFluctuationDoubleIntegral q =O[atTop] (fun x => log x ^ 2) ∧
      digitSumRemainderIntegral q =O[atTop] (fun _ => (1 : ℝ)) ∧
      digitSumRemainderDoubleIntegral q =O[atTop] log

Sources

• Ka Lun Wong and Erdenebileg Erdenebat, Asymptotics of Partial Sums of Dirichlet Convolutions of Digital Sum Functions in Arbitrary Bases, INTEGERS 26 (2026), Article A43, Lemma 3.

Uses 7

Statement usesDouble integral of the Trollope–Delange fluctuation · Integral of the Trollope–Delange fluctuation · Trollope–Delange remainder · Double integral of the Trollope–Delange remainder · Weighted integral of the Trollope–Delange remainder · Trollope–Delange fluctuation · Delange's series

TheoremBound for a weighted sum of the fluctuation#●ready to prove

Let \(q \ge 2\) be an integer, let \(s_q(n)\) denote the sum of the base-\(q\) digits of \(n\), let \(F\) be the Trollope–Delange fluctuation in base \(q\), and let \(F_M = \sup_{t \in \mathbb{R}} |F(t)|\) (taken to be \(0\) if \(|F|\) is unbounded). For all real numbers \(x > 0\) and \(y\),

\[\sum_{n=1}^{\lfloor y \rfloor} \frac{s_q(n)}{n} \, F\left(\frac{\log(x/n)}{\log q}\right) \le F_M \sum_{n=1}^{\lfloor y \rfloor} \frac{s_q(n)}{n}.\]

public theorem_wanted digitSum_reciprocal_fluctuation_sum_le (q : ℕ) (hq : 2 ≤ q) (x y : ℝ)
    (hx : 0 < x) :
    ∑ n ∈ Finset.Icc 1 ⌊y⌋₊,
        ((Nat.digits q n).sum : ℝ) / n * trollopeDelangeFluctuation q (log (x / n) / log q) ≤
      (⨆ t : ℝ, |trollopeDelangeFluctuation q t|) *
        ∑ n ∈ Finset.Icc 1 ⌊y⌋₊, ((Nat.digits q n).sum : ℝ) / n

Sources

• Ka Lun Wong and Erdenebileg Erdenebat, Asymptotics of Partial Sums of Dirichlet Convolutions of Digital Sum Functions in Arbitrary Bases, INTEGERS 26 (2026), Article A43, Lemma 4.

Uses 1

Statement usesTrollope–Delange fluctuation

TheoremReciprocal digit sums weighted by powers of the logarithm#●ready to prove

Let \(q \ge 2\) and \(j \ge 1\) be integers, and let \(s_q(n)\) denote the sum of the base-\(q\) digits of \(n\). As the real number \(x\) tends to infinity,

\[\sum_{n=1}^{\lfloor x \rfloor} \frac{s_q(n)}{n} \log^j n = \frac{(q - 1) \log^{j+2} x}{2 (j + 2) \log q} + O\left(\log^{j+1} x\right).\]

public theorem_wanted digitSum_reciprocal_log_pow_sum_isBigO (q : ℕ) (hq : 2 ≤ q) (j : ℕ)
    (hj : 1 ≤ j) :
    (fun x : ℝ => ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, ((Nat.digits q n).sum : ℝ) / n * log n ^ j -
        ((q : ℝ) - 1) * log x ^ (j + 2) / (2 * (j + 2) * log q)) =O[atTop]
      (fun x => log x ^ (j + 1))

Sources

• Ka Lun Wong and Erdenebileg Erdenebat, Asymptotics of Partial Sums of Dirichlet Convolutions of Digital Sum Functions in Arbitrary Bases, INTEGERS 26 (2026), Article A43, Lemma 5.

TheoremPartial sums of the second digit-sum convolution#●ready to prove

Let \(q \ge 2\) be an integer, let \(s_q(n)\) be the sum of the base-\(q\) digits of \(n\), and let \(s_q^{(2)} = s_q * s_q\) be its Dirichlet square, so \(s_q^{(2)}(n) = \sum_{de = n} s_q(d) \, s_q(e)\). Then

\[\sum_{1 \le n \le x} s_q^{(2)}(n) = \frac{(q - 1)^2}{24 \log^2 q} \, x \log^3 x + O(x \log^2 x)\]

as \(x \to \infty\) through the reals.

public theorem_wanted digitSumArith_sq_partialSum_isBigO (q : ℕ) (hq : 2 ≤ q) :
    (fun x : ℝ => ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, ((digitSumArith q ^ 2) n : ℝ) -
        ((q : ℝ) - 1) ^ 2 * x * log x ^ 3 / (24 * log q ^ 2)) =O[atTop]
      (fun x => x * log x ^ 2)

Sources

• Ka Lun Wong and Erdenebileg Erdenebat, Asymptotics of Partial Sums of Dirichlet Convolutions of Digital Sum Functions in Arbitrary Bases, INTEGERS 26 (2026), Article A43, Theorem 2.

Uses 1

Statement usesDigit-sum arithmetic function

TheoremPartial sums of the iterated digit-sum convolutions#●ready to prove

Let \(q \ge 2\) be an integer, let \(s_q(n)\) be the sum of the base-\(q\) digits of \(n\), let \(s_q^{(k)}\) be the \(k\)-fold Dirichlet convolution \(s_q * \cdots * s_q\), and let \(a(k)\) be the base-\(q\) digit-convolution coefficients. For every integer \(k \ge 2\),

\[\sum_{1 \le n \le x} s_q^{(k)}(n) = a(k) \, x \log^{2k-1} x + O(x \log^{2k-2} x)\]

as \(x \to \infty\) through the reals.

public theorem_wanted digitSumArith_pow_partialSum_isBigO (q : ℕ) (hq : 2 ≤ q) (k : ℕ)
    (hk : 2 ≤ k) :
    (fun x : ℝ => ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, ((digitSumArith q ^ k) n : ℝ) -
        digitConvolutionCoeff q k * x * log x ^ (2 * k - 1)) =O[atTop]
      (fun x => x * log x ^ (2 * k - 2))

Sources

• Ka Lun Wong and Erdenebileg Erdenebat, Asymptotics of Partial Sums of Dirichlet Convolutions of Digital Sum Functions in Arbitrary Bases, INTEGERS 26 (2026), Article A43, Theorem 3, equation (2).

Uses 2

Statement usesDigit-convolution coefficients · Digit-sum arithmetic function

22 fully proved8 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.