Hyperbolic floor sums of arithmetic functions

TheoremAbsolute convergence of a log-weighted difference series#●ready to prove

Let \(f\) be a real function on the natural numbers with \(f(n) = O(n^\alpha)\) as \(n \to \infty\) for some real \(\alpha\) with \(0 \le \alpha < 1\). Then for every natural number \(i\) the series

\[\sum_{n \ge 1} f(n) \left( \frac{(\log n)^i}{n} - \frac{(\log (n+1))^i}{n+1} \right)\]

converges absolutely.

public theorem_wanted summable_abs_mul_log_pow_div_sub
    (f : ℕ → ℝ) (α : ℝ) (hα0 : 0 ≤ α) (hα1 : α < 1)
    (hf : (fun n : ℕ => f n) =O[atTop] fun n : ℕ => (n : ℝ) ^ α) (i : ℕ) :
    Summable fun n : ℕ =>
      |f (n + 1) * (Real.log (n + 1) ^ i / (n + 1) - Real.log (n + 2) ^ i / (n + 2))|

Sources

• Meselem Karras and Mihoub Bouderbala, Hyperbolic Summation Involving Certain Arithmetic Functions and the Integer Part Function, INTEGERS 26 (2026), Article A37, Lemma 1.

TheoremAsymptotics of hyperbolic floor sums#●ready to prove

Let \(r \ge 2\) and let \(\tau_r(n)\) be the number of ordered factorizations \(n = n_1 \cdots n_r\) of \(n\) into \(r\) positive factors. Let \(P(t) = \sum_j a_j t^j\) be a real polynomial with \(\sum_{1 \le n \le x} \tau_r(n) - x P(\log x) = O(x^{1 - 1/r} (\log x)^{r-2})\) as \(x \to \infty\). Let \(f\) be a nonnegative real function on the natural numbers such that, for some real \(\alpha\) with \(0 \le \alpha < 1\), \(f(n) = O(n^\alpha)\) as \(n \to \infty\), and, for some real \(\beta \ge 0\), \(\sum_{1 \le n \le x} f(n) = O(x (\log \log x)^\beta)\) as \(x \to \infty\). For \(i \ge 0\) let

\[C_i = \sum_{n \ge 1} f(n) \left( \frac{(\log n)^i}{n} - \frac{(\log (n+1))^i}{n+1} \right).\]

Then, as \(x \to \infty\),

\[\sum_{1 \le n \le x} f(\lfloor x/n \rfloor) \, \tau_r(n) = x \sum_{j=0}^{r-1} \sum_{i=0}^{j} \binom{j}{i} (-1)^i a_j C_i (\log x)^{j-i} + O(x (\log x)^{r-2} (\log \log x)^\beta).\]

The hypothesis \(f \ge 0\) is not in the source: its proof bounds the error sum \(\sum_{d \le x} f(d) \, O((x/d)^{1-1/r} (\log (x/d))^{r-2})\) through \(\sum_{n \le x} f(n)\), which controls it only for nonnegative \(f\).

MetaMathlibExt.hyperbolic_floor_sum_asymptotic · 19 lines

public theorem_wanted hyperbolic_floor_sum_asymptotic
    (r : ℕ) (hr : 2 ≤ r) (P : Polynomial ℝ)
    (hP : (fun x : ℝ =>
        (∑ n ∈ Finset.Icc 1 ⌊x⌋₊, ((Nat.finMulAntidiag r n).card : ℝ)) -
          x * P.eval (Real.log x)) =O[atTop]
        fun x : ℝ => x ^ (1 - 1 / (r : ℝ)) * Real.log x ^ (r - 2))
    (f : ℕ → ℝ) (hf0 : ∀ n, 0 ≤ f n) (α : ℝ) (hα0 : 0 ≤ α) (hα1 : α < 1)
    (hf : (fun n : ℕ => f n) =O[atTop] fun n : ℕ => (n : ℝ) ^ α)
    (β : ℝ) (hβ : 0 ≤ β)
    (hsum : (fun x : ℝ => ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, f n) =O[atTop]
        fun x : ℝ => x * Real.log (Real.log x) ^ β) :
    (fun x : ℝ =>
        (∑ n ∈ Finset.Icc 1 ⌊x⌋₊, f ⌊x / n⌋₊ * ((Nat.finMulAntidiag r n).card : ℝ)) -
          x * ∑ j ∈ Finset.range r, ∑ i ∈ Finset.range (j + 1),
            (j.choose i : ℝ) * (-1) ^ i * P.coeff j *
              (∑' n : ℕ, f (n + 1) *
                (Real.log (n + 1) ^ i / (n + 1) - Real.log (n + 2) ^ i / (n + 2))) *
              Real.log x ^ (j - i)) =O[atTop]
      fun x : ℝ => x * Real.log x ^ (r - 2) * Real.log (Real.log x) ^ β

Sources

• Meselem Karras and Mihoub Bouderbala, Hyperbolic Summation Involving Certain Arithmetic Functions and the Integer Part Function, INTEGERS 26 (2026), Article A37, Theorem 1.

TheoremHyperbolic floor sums of additive functions of prime exponents#●ready to prove

Let \(r \ge 2\) and let \(\tau_r(n)\) be the number of ordered factorizations \(n = n_1 \cdots n_r\) of \(n\) into \(r\) positive factors. Let \(P(t) = \sum_j a_j t^j\) be a real polynomial with \(\sum_{1 \le n \le x} \tau_r(n) - x P(\log x) = O(x^{1 - 1/r} (\log x)^{r-2})\) as \(x \to \infty\). Let \(g\) be a real function on the natural numbers with \(g(1) \ne 0\) and \(g(a) = O(2^{a/2})\) as \(a \to \infty\). For \(n \ge 1\) let \(f(n) = \sum_{p \mid n} g(v_p(n))\), the sum over the primes \(p\) dividing \(n\), where \(v_p(n)\) is the exponent of \(p\) in \(n\), and for \(i \ge 0\) let

\[C_i = \sum_{n \ge 1} f(n) \left( \frac{(\log n)^i}{n} - \frac{(\log (n+1))^i}{n+1} \right).\]

Then, as \(x \to \infty\),

\[\sum_{1 \le n \le x} f(\lfloor x/n \rfloor) \, \tau_r(n) = x \sum_{j=0}^{r-1} \sum_{i=0}^{j} \binom{j}{i} (-1)^i a_j C_i (\log x)^{j-i} + O(x (\log x)^{r-2} \log \log x).\]

Since \(f(n)\) sums only over the primes dividing \(n\), the source's convention \(g(0) = 0\) is not needed.

MetaMathlibExt.hyperbolic_floor_sum_asymptotic_additive · 18 lines

public theorem_wanted hyperbolic_floor_sum_asymptotic_additive
    (r : ℕ) (hr : 2 ≤ r) (P : Polynomial ℝ)
    (hP : (fun x : ℝ =>
        (∑ n ∈ Finset.Icc 1 ⌊x⌋₊, ((Nat.finMulAntidiag r n).card : ℝ)) -
          x * P.eval (Real.log x)) =O[atTop]
        fun x : ℝ => x ^ (1 - 1 / (r : ℝ)) * Real.log x ^ (r - 2))
    (g : ℕ → ℝ) (hg1 : g 1 ≠ 0)
    (hg : (fun n : ℕ => g n) =O[atTop] fun n : ℕ => (2 : ℝ) ^ ((n : ℝ) / 2)) :
    (fun x : ℝ =>
        (∑ n ∈ Finset.Icc 1 ⌊x⌋₊,
            (∑ p ∈ (⌊x / n⌋₊).primeFactors, g ((⌊x / n⌋₊).factorization p)) *
              ((Nat.finMulAntidiag r n).card : ℝ)) -
          x * ∑ j ∈ Finset.range r, ∑ i ∈ Finset.range (j + 1),
            (j.choose i : ℝ) * (-1) ^ i * P.coeff j *
              (∑' n : ℕ, (∑ p ∈ (n + 1).primeFactors, g ((n + 1).factorization p)) *
                (Real.log (n + 1) ^ i / (n + 1) - Real.log (n + 2) ^ i / (n + 2))) *
              Real.log x ^ (j - i)) =O[atTop]
      fun x : ℝ => x * Real.log x ^ (r - 2) * Real.log (Real.log x)

Sources

• Meselem Karras and Mihoub Bouderbala, Hyperbolic Summation Involving Certain Arithmetic Functions and the Integer Part Function, INTEGERS 26 (2026), Article A37, Proposition 1.

3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.