A power-saving asymptotic for a Möbius-weighted GCD quadratic form

Ahmadreza Azimifard

math.NT Oct 31, 2026 · v1

Read PDF arXiv abstract

TL;DR

The main theorem's asymptotic, error estimate, convergence and positivity of the constant are formalized in Lean 4 with Mathlib, using no extra axioms.

Abstract

For the Möbius-weighted quadratic form $T(N)=\sum_{m,n\leq N}μ(m)μ(n)(m,n)^2/(mn)$, we prove that $T(N)=cN+O_{\varepsilon}(N^{2/3+\varepsilon})$ for every $\varepsilon>0$, where $c>0$ is given by an absolutely convergent series of finite Möbius sums multiplied by a convergent Euler product. The proof combines the classical Jordan-totient decomposition of the GCD kernel with a mean-value estimate that is uniform in a coprimality parameter. Grouping the resulting squares according to $\lfloor N/d\rfloor$ gives the error term and a nonnegative series for $c$.

Problem

The goal is to determine the asymptotic behaviour of the Möbius-weighted GCD quadratic form T(N)=Σ_{m,n≤N} μ(m)μ(n)(m,n)^2/(mn), including its linear term and a power-saving remainder.

Approach

The GCD kernel is decomposed via the Jordan totient J_2, which writes T(N) as a sum of nonnegative squares. A mean-value estimate for a multiplicative function, uniform in a coprimality parameter, is applied on hyperbola blocks where ⌊N/d⌋ is constant. Balancing the block errors against a direct bound for the remaining squares gives the exponent. The full result is formalized in Lean 4.28.0 with Mathlib.

Results

T(N)=cN+O_ε(N^{2/3+ε}), where c≥C_0/2>0 is given by a nonnegative absolutely convergent series. The Lean theorem depends only on the standard axioms, with no admitted propositions. Numerically, T(10^6)/10^6≈0.33112, consistent with the computed value of c.

Papers With

A power-saving asymptotic for a Möbius-weighted GCD quadratic form