Wintner's mean-value theorem

TheoremWintner's mean-value theorem#✓fully proved

Let \(f\) be a complex-valued arithmetic function, let \(\mu\) be the Möbius function, and let \(\mu * f\) be their Dirichlet convolution, \((\mu * f)(n) = \sum_{d \mid n} \mu(d) f(n/d)\). If the series \(\sum_{n \ge 1} |(\mu * f)(n)|/n\) converges, then

\[\frac{1}{x} \sum_{n=1}^{x} f(n) \to \sum_{n \ge 1} \frac{(\mu * f)(n)}{n}\]

as the integer \(x\) tends to infinity.

No multiplicativity, Euler product, quantitative error term, or alternating mean is assumed or concluded.

theorem wintner_mean_value (f : ArithmeticFunction ℂ)
    (hsum : Summable
      (fun n : ℕ => ‖((↑ArithmeticFunction.moebius : ArithmeticFunction ℂ) * f) n‖ /
        (n : ℝ))) :
  Filter.Tendsto (fun x : ℕ => ((x : ℂ)⁻¹) * ∑ n ∈ Finset.Icc 1 x, f n) Filter.atTop
    (nhds (∑' n : ℕ, ((↑ArithmeticFunction.moebius : ArithmeticFunction ℂ) * f) n /
      (n : ℂ)))

Sources

• László Tóth, On the Asymptotic Density of k-tuples of Positive Integers with Pairwise Non-Coprime Components, Journal of Integer Sequences 27 (2024), Article 24.8.5, mean-value definition and Theorem Th_Wintner_gen, lines 292–310 (the k = 1 case identified at lines 297–298 as Wintner's classical theorem; the source theorem itself is Ushiroya's multivariable generalization), https://cs.uwaterloo.ca/journals/JIS/VOL27/Toth/toth27.tex.

Used by 1

Used byEuler product for mean values of coordinatewise multiplicative functions

TheoremEuler product for mean values of coordinatewise multiplicative functions#✓fully proved

Let \(k\) be a natural number, write \(\mathbb{N} = \{0, 1, 2, \dots\}\), and let \(f \colon \mathbb{N}^k \to \mathbb{C}\) satisfy \(f(a_1 b_1, \dots, a_k b_k) = f(a) f(b)\) for all \(a, b \in \mathbb{N}^k\) with \(\gcd(a_i, b_i) = 1\) for every \(i\). For a prime \(p\) and \(\nu = (\nu_1, \dots, \nu_k) \in \mathbb{N}^k\) write \(p^\nu = (p^{\nu_1}, \dots, p^{\nu_k})\), \(|\nu| = \nu_1 + \dots + \nu_k\) and

\[ (\mu * f)(p^\nu) = \sum_{d_1 \mid p^{\nu_1}, \dots, d_k \mid p^{\nu_k}} \mu(d_1) \cdots \mu(d_k) \, f(p^{\nu_1} / d_1, \dots, p^{\nu_k} / d_k), \]

where \(\mu\) is the Möbius function and each \(d_i\) runs over the positive divisors of \(p^{\nu_i}\). Suppose that the family \(|(\mu * f)(p^\nu)| / p^{|\nu|}\), indexed by the pairs \((p, \nu)\) of a prime \(p\) and a nonzero \(\nu \in \mathbb{N}^k\), is summable. Then there is a complex number \(M\) such that

\[ \frac{1}{N^k} \sum_{n \in \{1, \dots, N\}^k} f(n) \to M \quad (N \to \infty) \]

and

\[ M = \prod_p \Bigl(1 - \frac{1}{p}\Bigr)^k \sum_{\nu \in \mathbb{N}^k} \frac{f(p^\nu)}{p^{|\nu|}}, \]

where the product runs over all primes and the product and the inner sums are unconditional (an unconditional sum that does not converge is read as \(0\), a product as \(1\)).

This is the Wintner–Ushiroya theorem (Ushiroya, Theorem 4; Tóth, Proposition 19) under a stronger multiplicativity hypothesis: the source asks for \(f(a_1 b_1, \dots, a_k b_k) = f(a) f(b)\) only when \(\gcd(a_1 \cdots a_k, b_1 \cdots b_k) = 1\). The hypothesis used here forces \(f\) to be a product of one-variable multiplicative functions of the coordinates, and the proof reduces to the one-variable Wintner theorem in each coordinate. The averages over the cubes \(\{1, \dots, N\}^k\) are the diagonal of the source's multi-parameter limit, so they converge to the same value.

MetaMathlibExt.euler_product_mean_value · 16 lines

public theorem euler_product_mean_value
    {k : ℕ} (f : (Fin k → ℕ) → ℂ)
    (hmult : ∀ a b : Fin k → ℕ, (∀ i, Nat.Coprime (a i) (b i)) →
      f (fun i => a i * b i) = f a * f b)
    (hsumm : Summable (fun q : { q : { p : ℕ // p.Prime } × (Fin k → ℕ) // q.2 ≠ 0 } =>
      ‖(∑ d ∈ Fintype.piFinset (fun i => Nat.divisors ((q.1.1 : ℕ) ^ (q.1.2 i))),
          (∏ i, ((ArithmeticFunction.moebius (d i) : ℤ) : ℂ)) *
          f (fun i => (q.1.1 : ℕ) ^ (q.1.2 i) / d i)) /
        (((q.1.1 : ℕ) : ℂ) ^ (∑ i, q.1.2 i))‖)) :
    ∃ M : ℂ, Filter.Tendsto (fun N : ℕ =>
      (∑ n ∈ Fintype.piFinset (fun _ : Fin k => Finset.Icc 1 N), f n) / ((N : ℂ) ^ k))
      Filter.atTop (nhds M) ∧
      M = ∏' (p : { p : ℕ // p.Prime }),
        ((1 - 1 / ((p : ℕ) : ℂ)) ^ k *
        (∑' (ν : Fin k → ℕ),
          f (fun i => (p : ℕ) ^ (ν i)) / (((p : ℕ) : ℂ) ^ (∑ i, ν i))))

Sources

• László Tóth, "On the Asymptotic Density of k-tuples of Positive Integers with Pairwise Non-Coprime Components," Journal of Integer Sequences 27 (2024), Article 24.8.5, Theorem (unlabeled; multiplicative-function form), equation, lines 314–326, https://cs.uwaterloo.ca/journals/JIS/VOL27/Toth/toth27.tex

Uses 1

Proof usesWintner's mean-value theorem

TheoremWintner's mean-value theorem in several variables#✓fully proved

Let \(k \ge 1\) and let \(f\) be a complex-valued function on \(k\)-tuples of natural numbers. For a \(k\)-tuple \(n = (n_1, \dots, n_k)\) of positive integers put

\[ (\mu * f)(n) = \sum_{d_1 \mid n_1, \dots, d_k \mid n_k} \mu(d_1) \cdots \mu(d_k) \, f(n_1/d_1, \dots, n_k/d_k), \]

where \(\mu\) is the Möbius function and the \(d_i\) run over positive divisors. If the series

\[\sum_{m \in \mathbb{Z}_{\ge 1}^k} \frac{|(\mu * f)(m)|}{m_1 \cdots m_k}\]

converges, then

\[ \frac{1}{x_1 \cdots x_k} \sum_{n_1 = 1}^{x_1} \cdots \sum_{n_k = 1}^{x_k} f(n_1, \dots, n_k) \to \sum_{m \in \mathbb{Z}_{\ge 1}^k} \frac{(\mu * f)(m)}{m_1 \cdots m_k} \]

as the integers \(x_1, \dots, x_k\) all tend to infinity.

MetaMathlibExt.wintner_mean_value_multivariable · 19 lines

theorem wintner_mean_value_multivariable
    (k : ℕ) (hk : 0 < k) (f : (Fin k → ℕ) → ℂ) :
    let mobiusConvolution : (Fin k → ℕ) → ℂ := (fun n =>
      ∑ d : (i : Fin k) → Fin (n i),
        if ∀ i, (d i : ℕ) + 1 ∣ n i then
          (∏ i, (ArithmeticFunction.moebius ((d i : ℕ) + 1) : ℂ)) *
            f (fun i => n i / ((d i : ℕ) + 1))
        else 0);
    Summable (fun m : Fin k → ℕ =>
      ‖mobiusConvolution (fun i => m i + 1)‖ /
        ∏ i, (m i + 1 : ℝ)) →
      Filter.Tendsto
        (fun x : Fin k → ℕ =>
          (∑ n : (i : Fin k) → Fin (x i), f (fun i => (n i : ℕ) + 1)) /
            ∏ i, (x i : ℂ))
        Filter.atTop
        (nhds (∑' m : Fin k → ℕ,
          mobiusConvolution (fun i => m i + 1) /
            ∏ i, (m i + 1 : ℂ)))

Sources

• László Tóth, "On the Asymptotic Density of k-tuples of Positive Integers with Pairwise Non-Coprime Components," Journal of Integer Sequences 27 (2024), Article 24.8.5, Theorem Th_Wintner_gen, lines 300–311, https://cs.uwaterloo.ca/journals/JIS/VOL27/Toth/toth27.tex. Proved by H. Ushiroya (2012) as a generalization of Wintner's classical one-variable theorem.

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.