Multiplicative functions and mean values

Dirichlet and unitary convolution, completely multiplicative and additive functions, Wintner and Euler-product mean values, additive uniqueness sets, Mertens bounds.

• Additive uniqueness of multiplicative functions
• Completely additive height functions
• Completely multiplicative functions
• Hyperbolic floor sums of arithmetic functions
• Multiplicative functions in short intervals
• Möbius–Fermat function
• Random multiplicative functions
• Rearick logarithm
• Antimultiplicative arithmetic functions
• Square-splitting convolution
• Tuples coprime along the edges of a graph
• Unitary convolution
• Vaughan's identity
• Weighted sums of Dirichlet convolutions
• Wintner's mean-value theorem

TheoremExplicit bounds for the summatory function of \(\mu(n)/n\)#●ready to prove

Let \(\mu\) be the Möbius function. For every real \(x \ge 33\),

\[\Bigl| \sum_{1 \le n \le x} \frac{\mu(n)}{n} \Bigr| < \frac{0.19}{\log x},\]

and for every real \(x > 1\),

\[\Bigl| \sum_{1 \le n \le x} \frac{\mu(n)}{n} \Bigr| < \frac{546}{(\log x)^2}.\]

These bounds improve the estimates \(0.2185/\log x\) and \(726/(\log x)^2\) of the source's equation (e4).

public theorem_wanted summatory_moebius_div_bound :
    (∀ x : ℝ, 33 ≤ x →
      |∑ n ∈ Finset.Icc 1 ⌊x⌋₊, (ArithmeticFunction.moebius n : ℝ) / n| <
        (0.19 : ℝ) / Real.log x) ∧
    (∀ x : ℝ, 1 < x →
      |∑ n ∈ Finset.Icc 1 ⌊x⌋₊, (ArithmeticFunction.moebius n : ℝ) / n| <
        546 / (Real.log x) ^ 2)

Sources

• Olivier Bordellès, "Some Explicit Estimates for the Möbius Function," Journal of Integer Sequences 18 (2015), Article 15.11.1, Theorem, items (a) and (b), lines 118–127, https://cs.uwaterloo.ca/journals/JIS/VOL18/Bordelles2/bordelles21.tex

TheoremPrime powers fixed by a uniform power sum of their prime factors#✓fully proved

For positive integers \(y\) and \(s\), let \(T_s(y) = \sum_q e_q q^s\), where \(q\) runs over the primes dividing \(y\) and \(e_q\) is the exponent of \(q\) in \(y\), so that each prime factor is counted with multiplicity. Let \(p\) be a prime, let \(m\) be a positive integer and let \(y = p^m\). Then for every positive integer \(s\), \(T_s(y) = y\) if and only if \(m = p^k\) and \(s = p^k - k\) for some natural number \(k\).

For \(y = p^m\) one has \(T_s(y) = m p^s\), and \(m p^s = p^m\) forces \(m\) to be a power of \(p\).

theorem prime_power_factorization_sum_eq_iff
    {p m s y : ℕ} (hp : Nat.Prime p) (hm : 0 < m) (hs : 0 < s)
    (hy : y = p ^ m) :
    (y.factorization.sum fun q e => e * q ^ s) = y ↔
      ∃ k : ℕ, m = p ^ k ∧ s = p ^ k - k

Sources

• Spencer P. Hurd and Judson S. McCranie, "Integers That Are Sums of Uniform Powers of All Their Prime Factors: The Sequence A068916," Journal of Integer Sequences 22 (2019), Article 19.3.4, Theorem 1, lines 187–189, https://cs.uwaterloo.ca/journals/JIS/VOL22/Hurd/hurd1.tex

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.