Pillai's gcd-sum function

TheoremDirichlet series of the gcd-sum function#✓fully proved

For \(n \ge 1\) let \(g(n) = \sum_{i=1}^{n} \gcd(n, i)\). For every complex number \(s\) with \(\operatorname{Re} s > 2\), the series \(\sum_{n \ge 1} g(n)/n^s\) sums to \(\zeta(s-1)^2/\zeta(s)\), where \(\zeta\) is the Riemann zeta function.

The function \(g\) is the Dirichlet convolution of the identity function with Euler's totient function \(\varphi\), which gives the factorization \(\zeta(s-1) \cdot (\zeta(s-1)/\zeta(s))\).

theorem dirichlet_series_gcd_sum
    (s : ℂ) (hs : 2 < s.re) :
    (∑' n : ℕ, ((∑ i ∈ Finset.range (n + 1), (Nat.gcd (n + 1) (i + 1) : ℂ))
      / (((n + 1 : ℕ) : ℂ)) ^ s))
      = riemannZeta (s - 1) ^ 2 / riemannZeta s
Sources
  • Kevin A. Broughan, "The gcd-sum function," Journal of Integer Sequences 4 (2001), Article 01.2.2, Theorem (unlabeled), equations (labels 12, 8), lines 336–349, https://cs.uwaterloo.ca/journals/JIS/VOL4/BROUGHAN/gcdsum.tex

TheoremThe gcd-sum as a divisor sum of totients#✓fully proved

For every positive integer \(n\), \(\sum_{j=1}^{n} \gcd(j, n) = n \sum_{d \mid n} \varphi(d)/d\), where \(\varphi\) is Euler's totient function and \(d\) runs over the positive divisors of \(n\).

Grouping the terms with \(\gcd(j, n) = e\), of which there are \(\varphi(n/e)\), shows that the sum equals \(\sum_{e \mid n} e \, \varphi(n/e)\).

theorem gcd_sum_eq_totient_sum
    (n : ℕ) (hn : 0 < n) :
    (∑ j ∈ Finset.Icc 1 n, (Nat.gcd j n : ℚ)) =
      (n : ℚ) * ∑ d ∈ Nat.divisors n, (Nat.totient d : ℚ) / (d : ℚ)
Sources
  • Kevin A. Broughan, "The Gcd-Sum Function," Journal of Integer Sequences 4 (2001), Article 01.2.2, Theorem 2.3, lines 220–226, https://cs.uwaterloo.ca/journals/JIS/VOL4/BROUGHAN/gcdsum.tex
Used by 1
Used byDivisor-sum formula for the mean gcd-sum function

DefinitionThe mean gcd-sum function#✓fully proved

For a natural number \(n\), let \(P(n) = \sum_{j=1}^{n} \gcd(j, n)\) be Pillai's gcd-sum function. The mean gcd-sum function is the real-valued function given by \(A(n) = P(n)/n\) for \(n \ge 1\) and \(A(0) = 0\).

noncomputable def gcdSumMean (n : ℕ) : ℝ :=
  (∑ j ∈ Finset.Icc 1 n, (Nat.gcd j n : ℝ)) / n
Sources
  • M. S. Datt, Ekta Soni, and A. Sankaranarayanan, On the Asymptotic Formula for the Gcd-Sum Function, INTEGERS 26 (2026), Article A70, Section 1 (definition of A(n)).
Used by 11
Used byDivisor-sum formula for the mean gcd-sum function · The mean gcd-sum function at \(1\) · Integral of the error term for gcd-sum moments under RH · Mean square of the error term for gcd-sum moments under RH · The mean gcd-sum function at \(2\) · Factorization of the Dirichlet series of powers of the mean gcd-sum function · Dirichlet series of the square of the mean gcd-sum function · Asymptotic formula for the third moment of the mean gcd-sum function · Asymptotic formula for the higher moments of the mean gcd-sum function · Asymptotic formula for the fourth moment of the mean gcd-sum function · Asymptotic formula for the second moment of the mean gcd-sum function

TheoremThe mean gcd-sum function at \(1\)#✓fully proved

The mean gcd-sum function \(A\) satisfies \(A(1) = 1\).

theorem gcdSumMean_one : gcdSumMean 1 = 1
Sources
  • M. S. Datt, Ekta Soni, and A. Sankaranarayanan, On the Asymptotic Formula for the Gcd-Sum Function, INTEGERS 26 (2026), Article A70, Section 1 (definition of A(n)).
Uses 1
Statement usesThe mean gcd-sum function

TheoremThe mean gcd-sum function at \(2\)#✓fully proved

The mean gcd-sum function \(A\) satisfies \(A(2) = 3/2\), since \(A(2) = P(2)/2\), where \(P(n) = \sum_{j=1}^{n} \gcd(j, n)\) is Pillai's gcd-sum function and \(P(2) = \gcd(1, 2) + \gcd(2, 2) = 3\).

theorem gcdSumMean_two : gcdSumMean 2 = 3 / 2
Sources
  • M. S. Datt, Ekta Soni, and A. Sankaranarayanan, On the Asymptotic Formula for the Gcd-Sum Function, INTEGERS 26 (2026), Article A70, Section 1 (definition of A(n)).
Uses 1
Statement usesThe mean gcd-sum function

TheoremDivisor-sum formula for the mean gcd-sum function#✓fully proved

For every natural number \(n \ge 1\), the mean gcd-sum function \(A\) satisfies \(A(n) = \sum_{d \mid n} \varphi(d)/d\), where \(\varphi\) is Euler's totient function and the sum runs over the positive divisors \(d\) of \(n\).

theorem gcdSumMean_eq_sum_totient_div {n : ℕ} (hn : 0 < n) :
    gcdSumMean n = ∑ d ∈ n.divisors, (Nat.totient d : ℝ) / d
Sources
  • M. S. Datt, Ekta Soni, and A. Sankaranarayanan, On the Asymptotic Formula for the Gcd-Sum Function, INTEGERS 26 (2026), Article A70, Section 1 (Pillai's identity).
Uses 2
Statement usesThe mean gcd-sum function
Proof usesThe gcd-sum as a divisor sum of totients

TheoremAsymptotic formula for the second moment of the mean gcd-sum function#●ready to prove

For \(n \ge 1\) let \(A(n) = \frac{1}{n} \sum_{j=1}^{n} \gcd(j, n)\) be the mean gcd-sum function. There are a real polynomial \(P\) and a real constant \(C\) such that, as \(x \to \infty\),

\[\sum_{1 \le n \le x} A(n)^2 = x P(\log x) + O\left(x^{1/2} \exp\left(C (\log \log x)^2\right)\right).\]
public theorem_wanted sum_gcdSumMean_sq_asymptotic :
    ∃ (P : ℝ[X]) (C : ℝ),
      (fun x : ℝ => ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, gcdSumMean n ^ 2 - x * P.eval (Real.log x))
        =O[atTop] fun x => x ^ (1 / 2 : ℝ) * Real.exp (C * Real.log (Real.log x) ^ 2)
Sources
  • M. S. Datt, Ekta Soni, and A. Sankaranarayanan, On the Asymptotic Formula for the Gcd-Sum Function, INTEGERS 26 (2026), Article A70, Theorem 1.
Uses 1
Statement usesThe mean gcd-sum function

TheoremAsymptotic formula for the third moment of the mean gcd-sum function#●ready to prove

For \(n \ge 1\) let \(A(n) = \frac{1}{n} \sum_{j=1}^{n} \gcd(j, n)\) be the mean gcd-sum function. There are a real polynomial \(P\) and a real constant \(C\) such that, as \(x \to \infty\),

\[\sum_{1 \le n \le x} A(n)^3 = x P(\log x) + O\left(x^{5/8} \exp\left(C (\log \log x)^2\right)\right).\]
public theorem_wanted sum_gcdSumMean_cube_asymptotic :
    ∃ (P : ℝ[X]) (C : ℝ),
      (fun x : ℝ => ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, gcdSumMean n ^ 3 - x * P.eval (Real.log x))
        =O[atTop] fun x => x ^ (5 / 8 : ℝ) * Real.exp (C * Real.log (Real.log x) ^ 2)
Sources
  • M. S. Datt, Ekta Soni, and A. Sankaranarayanan, On the Asymptotic Formula for the Gcd-Sum Function, INTEGERS 26 (2026), Article A70, Theorem 2.
Uses 1
Statement usesThe mean gcd-sum function

TheoremAsymptotic formula for the fourth moment of the mean gcd-sum function#●ready to prove

For \(n \ge 1\) let \(A(n) = \frac{1}{n} \sum_{j=1}^{n} \gcd(j, n)\) be the mean gcd-sum function. There is a real polynomial \(P\) such that for every \(\varepsilon > 0\), as \(x \to \infty\),

\[\sum_{1 \le n \le x} A(n)^4 = x P(\log x) + O_\varepsilon\left(x^{157/199 + \varepsilon}\right).\]
public theorem_wanted sum_gcdSumMean_pow_four_asymptotic :
    ∃ P : ℝ[X], ∀ ε : ℝ, 0 < ε →
      (fun x : ℝ => ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, gcdSumMean n ^ 4 - x * P.eval (Real.log x))
        =O[atTop] fun x => x ^ (157 / 199 + ε)
Sources
  • M. S. Datt, Ekta Soni, and A. Sankaranarayanan, On the Asymptotic Formula for the Gcd-Sum Function, INTEGERS 26 (2026), Article A70, Theorem 3.
Uses 1
Statement usesThe mean gcd-sum function

TheoremAsymptotic formula for the higher moments of the mean gcd-sum function#●ready to prove

For \(n \ge 1\) let \(A(n) = \frac{1}{n} \sum_{j=1}^{n} \gcd(j, n)\) be the mean gcd-sum function, and let \(k \ge 5\) be an integer. There is a real polynomial \(P\) such that for every \(\varepsilon > 0\), as \(x \to \infty\),

\[\sum_{1 \le n \le x} A(n)^k = x P(\log x) + O_{k,\varepsilon}\left(x^{1 + 2\varepsilon - 42/(13 \cdot 2^k - 9)}\right).\]
public theorem_wanted sum_gcdSumMean_pow_asymptotic (k : ℕ) (hk : 5 ≤ k) :
    ∃ P : ℝ[X], ∀ ε : ℝ, 0 < ε →
      (fun x : ℝ => ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, gcdSumMean n ^ k - x * P.eval (Real.log x))
        =O[atTop] fun x => x ^ (1 + 2 * ε - 42 / (13 * 2 ^ k - 9))
Sources
  • M. S. Datt, Ekta Soni, and A. Sankaranarayanan, On the Asymptotic Formula for the Gcd-Sum Function, INTEGERS 26 (2026), Article A70, Theorem 4.
Uses 1
Statement usesThe mean gcd-sum function

TheoremFactorization of the Dirichlet series of powers of the mean gcd-sum function#●ready to prove

Let \(k\) be a natural number and let \(A\) be the mean gcd-sum function. There are functions \(g, h \colon \mathbb{N} \to \mathbb{C}\) such that the Dirichlet series \(G_k(s) = \sum_{n \ge 1} g(n) n^{-s}\) converges absolutely for every complex \(s\) with \(\operatorname{Re} s > 1/2\), the Dirichlet series \(\tilde G_{k,2}(s) = \sum_{n \ge 1} h(n) n^{-s}\) converges absolutely for every complex \(s\) with \(\operatorname{Re} s > 1/3\), and for every complex \(s\) with \(\operatorname{Re} s > 1\),

\[\sum_{n \ge 1} A(n)^k n^{-s} = \zeta(s)^{2^k} G_k(s)\]

and

\[G_k(s) \, \zeta(2s)^{4^k - 3^k - \binom{2^k}{2}} = \tilde G_{k,2}(s).\]

The exponent \(4^k - 3^k - \binom{2^k}{2}\) is a nonnegative integer, since \(3^k + \binom{2^k}{2} \le 4^k\). The paper also gives an explicit Euler product for \(\tilde G_{k,2}\), which is not stated here.

public theorem_wanted LSeries_gcdSumMean_pow_eq_riemannZeta_pow_mul (k : ℕ) :
    ∃ g h : ℕ → ℂ, (∀ s : ℂ, 1 / 2 < s.re → LSeriesSummable g s) ∧
      (∀ s : ℂ, 1 / 3 < s.re → LSeriesSummable h s) ∧
      ∀ s : ℂ, 1 < s.re →
        LSeries (fun n => ((gcdSumMean n ^ k : ℝ) : ℂ)) s = riemannZeta s ^ (2 ^ k) * LSeries g s ∧
        LSeries g s * riemannZeta (2 * s) ^ (4 ^ k - 3 ^ k - (2 ^ k).choose 2) = LSeries h s
Sources
  • M. S. Datt, Ekta Soni, and A. Sankaranarayanan, On the Asymptotic Formula for the Gcd-Sum Function, INTEGERS 26 (2026), Article A70, Lemma 8.
Uses 1
Statement usesThe mean gcd-sum function

TheoremAn alternating binomial sum vanishes#●ready to prove

Let \(k\) and \(m\) be natural numbers with \(k \ge 2\) and \(m \ge 2^k - 1\). Then, computed in the integers,

\[\sum_{r=0}^{\min(2^k,\, m+1)} (-1)^r \binom{2^k}{r} (m + 1 - r)^k = 0.\]

Since \(m + 1 \ge 2^k\), the upper limit of the sum is \(2^k\).

This sum is the exponent \(\ell_m\) of the paper: the coefficient of \(p^{-ms}\) in \((1 - p^{-s})^{2^k} \sum_{a \ge 0} (a + 1)^k p^{-as}\), which is why it stops at \(r = m + 1\). The paper prints the sum up to \(r = 2^k\) for every \(m\); that sum vanishes for every \(m\), being a \(2^k\)-th difference of a polynomial of degree \(k\), which contradicts the paper's own \(\ell_2 = 3^k - 4^k + \binom{2^k}{2}\): for \(k = m = 2\) the truncated sum is \(-1\). So with the truncation the hypothesis \(m \ge 2^k - 1\) is needed. The paper's hypothesis \(k \ge 2\) is kept: for \(k = 0\) the term \(r = m + 1\) contributes \(0^0 = 1\) rather than the coefficient of a negative index, so the truncated sum is no longer the coefficient read off from the paper's Euler product.

public theorem_wanted alternating_choose_two_pow_mul_pow_eq_zero (k m : ℕ) (hk : 2 ≤ k)
    (hm : 2 ^ k - 1 ≤ m) :
    ∑ r ∈ Finset.range (min (2 ^ k) (m + 1) + 1),
      (-1 : ℤ) ^ r * ((2 ^ k).choose r : ℤ) * ((m : ℤ) + 1 - r) ^ k = 0
Sources
  • M. S. Datt, Ekta Soni, and A. Sankaranarayanan, On the Asymptotic Formula for the Gcd-Sum Function, INTEGERS 26 (2026), Article A70, Theorem 5.

TheoremDirichlet series of the square of the mean gcd-sum function#●ready to prove

Let \(A\) be the mean gcd-sum function. There is a function \(h \colon \mathbb{N} \to \mathbb{C}\) such that the Dirichlet series \(\tilde G_{2,2}(s) = \sum_{n \ge 1} h(n) n^{-s}\) converges absolutely for every complex \(s\) with \(\operatorname{Re} s > 0\), and for every complex \(s\) with \(\operatorname{Re} s > 1\),

\[\sum_{n \ge 1} A(n)^2 n^{-s} = \frac{\zeta(s)^4}{\zeta(2s)} \, \tilde G_{2,2}(s).\]

This is the case \(k = 2\) of the paper's Theorem 5, which gives the absolute convergence of \(\tilde G_{2,2}(s)\) in every half-plane \(\operatorname{Re} s > 1/N\) with \(N \ge 1\), that is, for \(\operatorname{Re} s > 0\).

public theorem_wanted LSeries_gcdSumMean_sq_eq_riemannZeta_pow_four_div :
    ∃ h : ℕ → ℂ, (∀ s : ℂ, 0 < s.re → LSeriesSummable h s) ∧
      ∀ s : ℂ, 1 < s.re →
        LSeries (fun n => ((gcdSumMean n ^ 2 : ℝ) : ℂ)) s =
          riemannZeta s ^ 4 / riemannZeta (2 * s) * LSeries h s
Sources
  • M. S. Datt, Ekta Soni, and A. Sankaranarayanan, On the Asymptotic Formula for the Gcd-Sum Function, INTEGERS 26 (2026), Article A70, Theorem 5.
Uses 1
Statement usesThe mean gcd-sum function

TheoremIvić's eighth-moment bound on the line \(\operatorname{Re} s = 5/8\)#●ready to prove

There are real constants \(C\) and \(T_0\) such that for every real \(T \ge T_0\),

\[\int_{T/2}^{T} |\zeta(5/8 + it)|^8 \, dt \le C T (\log T)^{38}.\]
public theorem_wanted riemannZeta_eighth_moment_five_eighths_le :
    ∃ C T₀ : ℝ, ∀ T : ℝ, T₀ ≤ T →
      ∫ t in T / 2..T, ‖riemannZeta (5 / 8 + t * I)‖ ^ 8 ≤ C * T * Real.log T ^ 38
Sources
  • M. S. Datt, Ekta Soni, and A. Sankaranarayanan, On the Asymptotic Formula for the Gcd-Sum Function, INTEGERS 26 (2026), Article A70, Lemma 2.

TheoremLemma 3#●ready to prove

Lemma 3 (quoted twelfth-moment asymptotic). For fixed 5/7 < σ < 1 and every ε > 0, ∫_1^T |ζ(σ + i t)|^{12} dt = T ∑_{n ≥ 1} d_6(n)^2 n^{-2σ} + O(T^{(9 - 7σ)/4 + ε}), where d_6 = ζ^{*6} is the six-fold divisor function. The printed side condition |t| ≥ 1 is implied by the integration range and omitted.

public theorem_wanted riemannZeta_twelfth_moment_asymptotic {σ : ℝ} (hσ₁ : 5 / 7 < σ)
    (hσ₂ : σ < 1) {ε : ℝ} (hε : 0 < ε) :
    (fun T : ℝ => ∫ t in (1 : ℝ)..T, ‖riemannZeta (σ + t * I)‖ ^ 12 -
        T * ∑' n : ℕ,
          ((ArithmeticFunction.zeta ^ 6 : ArithmeticFunction ℕ) n : ℝ) ^ 2 / (n : ℝ) ^ (2 * σ))
      =O[atTop] fun T => T ^ ((9 - 7 * σ) / 4 + ε)
Sources
  • M. S. Datt, Ekta Soni, and A. Sankaranarayanan, On the Asymptotic Formula for the Gcd-Sum Function, INTEGERS 26 (2026), Article A70, Lemma 3.

TheoremA weighted fourth-moment bound for \(\zeta\) on the critical line#●ready to prove

There are real constants \(C\) and \(T_0\) such that for every real \(T \ge T_0\),

\[\int_{10}^{T} \frac{|\zeta(1/2 + it)|^4}{|\zeta(1 + 2it)|} \, dt \le C T (\log T)^5.\]
public theorem_wanted riemannZeta_fourth_moment_div_le :
    ∃ C T₀ : ℝ, ∀ T : ℝ, T₀ ≤ T →
      ∫ t in (10 : ℝ)..T, ‖riemannZeta (1 / 2 + t * I)‖ ^ 4 / ‖riemannZeta (1 + 2 * t * I)‖ ≤
        C * T * Real.log T ^ 5
Sources
  • M. S. Datt, Ekta Soni, and A. Sankaranarayanan, On the Asymptotic Formula for the Gcd-Sum Function, INTEGERS 26 (2026), Article A70, Lemma 5.

TheoremRamachandra–Sankaranarayanan bound for \(\zeta\) at a well-chosen height#●ready to prove

Let \(\zeta\) be the Riemann zeta function. There are real constants \(C\) and \(U_0\) such that for every real \(U \ge U_0\) there is a real number \(T\) with \(U < T < 2U\) such that for every real \(\sigma \ge 1/2\),

\[ |\zeta(\sigma + iT)| \le \exp\bigl(C (\log \log U)^2\bigr) \quad \text{and} \quad |\zeta(\sigma - iT)| \le \exp\bigl(C (\log \log U)^2\bigr). \]

The source adds that this bound is \(\ll U^{\varepsilon}\) for every \(\varepsilon > 0\); that consequence is not part of this statement.

public theorem_wanted exists_riemannZeta_norm_le_exp_loglog_sq :
    ∃ C U₀ : ℝ, ∀ U : ℝ, U₀ ≤ U → ∃ T ∈ Set.Ioo U (2 * U), ∀ σ : ℝ, 1 / 2 ≤ σ →
      ‖riemannZeta (σ + T * I)‖ ≤ Real.exp (C * Real.log (Real.log U) ^ 2) ∧
        ‖riemannZeta (σ - T * I)‖ ≤ Real.exp (C * Real.log (Real.log U) ^ 2)
Sources
  • M. S. Datt, Ekta Soni, and A. Sankaranarayanan, On the Asymptotic Formula for the Gcd-Sum Function, INTEGERS 26 (2026), Article A70, Lemma 7.

TheoremMean square of the error term for gcd-sum moments under RH#●ready to prove

Let \(A(n) = \frac{1}{n} \sum_{m=1}^{n} \gcd(m, n)\) be the mean gcd-sum function. Assume the Riemann Hypothesis and let \(k \ge 2\) be an integer. Then there is a real polynomial \(P\) with the following property. Write \(E(u) = \sum_{1 \le n \le u} A(n)^k - u P(\log u)\) for real \(u\). For every real \(\eta\) with \(\frac{1}{2^k}\left(4^k - 3^k - \binom{2^k}{2}\right) + \frac{1}{2^{k+1}} + 1 \le \eta\) there are real constants \(C\) and \(T_0\) such that for all real \(T \ge T_0\),

\[\int_1^T E(u)^2 \, du \le C \, T^{2 - 1/2^k} \exp\left(\frac{2 \eta \log T}{\log \log T}\right).\]
public theorem_wanted gcdSumMean_pow_error_sq_integral_le (hRH : RiemannHypothesis) (k : ℕ)
    (hk : 2 ≤ k) :
    ∃ P : ℝ[X], ∀ η : ℝ,
      ((4 : ℝ) ^ k - 3 ^ k - ((2 ^ k).choose 2 : ℕ)) / 2 ^ k + 1 / 2 ^ (k + 1) + 1 ≤ η →
      ∃ C T₀ : ℝ, ∀ T : ℝ, T₀ ≤ T →
        ∫ u in (1 : ℝ)..T,
            (∑ n ∈ Finset.Icc 1 ⌊u⌋₊, gcdSumMean n ^ k - u * P.eval (Real.log u)) ^ 2 ≤
          C * T ^ (2 - 1 / (2 : ℝ) ^ k) *
            Real.exp (2 * η * Real.log T / Real.log (Real.log T))
Sources
  • Isao Kiuchi and Yuki Tsuruta, Mean Square Estimates for GCD-Sum Functions, INTEGERS 25 (2025), Article A53, Theorem 1.
Uses 1
Statement usesThe mean gcd-sum function

TheoremIntegral of the error term for gcd-sum moments under RH#●ready to prove

Let \(A(n) = \frac{1}{n} \sum_{m=1}^{n} \gcd(m, n)\) be the mean gcd-sum function. Assume the Riemann Hypothesis and let \(k \ge 2\) be an integer. Then there is a real polynomial \(P\) with the following property. Write \(E(u) = \sum_{1 \le n \le u} A(n)^k - u P(\log u)\) for real \(u\). For every real \(\eta\) with \(\frac{1}{2^k}\left(4^k - 3^k - \binom{2^k}{2}\right) + \frac{1}{2^{k+1}} + 1 \le \eta\) there are real constants \(C\) and \(T_0\) such that for all real \(T \ge T_0\),

\[\left|\int_1^T E(u) \, du\right| \le C \, T^{3/2 - 1/2^{k+1}} \exp\left(\frac{\eta \log T}{\log \log T}\right).\]
public theorem_wanted gcdSumMean_pow_error_integral_le (hRH : RiemannHypothesis) (k : ℕ)
    (hk : 2 ≤ k) :
    ∃ P : ℝ[X], ∀ η : ℝ,
      ((4 : ℝ) ^ k - 3 ^ k - ((2 ^ k).choose 2 : ℕ)) / 2 ^ k + 1 / 2 ^ (k + 1) + 1 ≤ η →
      ∃ C T₀ : ℝ, ∀ T : ℝ, T₀ ≤ T →
        |∫ u in (1 : ℝ)..T,
            (∑ n ∈ Finset.Icc 1 ⌊u⌋₊, gcdSumMean n ^ k - u * P.eval (Real.log u))| ≤
          C * T ^ (3 / 2 - 1 / (2 : ℝ) ^ (k + 1)) *
            Real.exp (η * Real.log T / Real.log (Real.log T))
Sources
  • Isao Kiuchi and Yuki Tsuruta, Mean Square Estimates for GCD-Sum Functions, INTEGERS 25 (2025), Article A53, Corollary 1.
Uses 1
Statement usesThe mean gcd-sum function
6 fully proved13 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.