Vaughan's identity

TheoremVaughan's identity in a commutative ring#✓fully proved

Let \(R\) be a commutative ring, let \(\mu\) and \(\Lambda\) be arithmetic functions with values in \(R\) (so \(\mu(0) = \Lambda(0) = 0\)), and let \(L : \mathbb{N} \to R\) be any function. Suppose that for every natural number \(m\), \(\sum_{d \mid m} \mu(d)\) is \(1\) if \(m = 1\) and \(0\) otherwise, and \(\Lambda(m) = \sum_{d \mid m} \mu(d) \, L(m/d)\), where both sums run over the \(d\) with \(0 \le d \le m\) and \(d \mid m\). Then for all natural numbers \(U\), \(V\) and \(n\) with \(V < n\),

\[\Lambda(n) = \sum_{b \mid n,\ b \le U} \mu(b) \, L(n/b) - \sum_{b \mid n,\ b \le U} \ \sum_{c \le V,\ bc \mid n} \mu(b) \, \Lambda(c) + \sum_{b \mid n,\ b > U} \ \sum_{c > V,\ bc \mid n} \mu(b) \, \Lambda(c),\]

where \(b\) and \(c\) range over \(0, 1, \dots, n\).

When \(R = \mathbb{R}\), \(\mu\) is the Möbius function, \(L = \log\) and \(\Lambda\) is the von Mangoldt function, the hypotheses hold and this is the classical Vaughan identity.

MetaMathlibExt.vaughan_identity_general · 15 lines

theorem vaughan_identity_general {R : Type*} [CommRing R]
    (μ Λ : ArithmeticFunction R) (logW : ℕ → R)
    (U V n : ℕ) (hn : V < n)
    (hLambda : ∀ m, Λ m =
      ∑ d ∈ (Finset.range (m + 1)).filter (fun d => d ∣ m), μ d * logW (m / d))
    (hMu : ∀ m, ∑ d ∈ (Finset.range (m + 1)).filter (fun d => d ∣ m), μ d =
      if m = 1 then 1 else 0) :
    Λ n = (∑ b ∈ (Finset.range (n + 1)).filter (fun b => b ∣ n ∧ b ≤ U),
        μ b * logW (n / b))
      - (∑ b ∈ (Finset.range (n + 1)).filter (fun b => b ∣ n ∧ b ≤ U),
          ∑ c ∈ (Finset.range (n + 1)).filter (fun c => c ≤ V ∧ b * c ∣ n),
            μ b * Λ c)
      + (∑ b ∈ (Finset.range (n + 1)).filter (fun b => b ∣ n ∧ U < b),
          ∑ c ∈ (Finset.range (n + 1)).filter (fun c => V < c ∧ b * c ∣ n),
            μ b * Λ c)

Used by 1

Used byVaughan's identity

TheoremVaughan's identity#✓fully proved

Let \(R\) be a commutative ring, let \(\mu\) and \(\Lambda\) be arithmetic functions with values in \(R\) (so \(\mu(0) = \Lambda(0) = 0\)), and let \(L : \mathbb{N} \to R\) be any function. Suppose that for every natural number \(m\), \(\sum_{d \mid m} \mu(d)\) is \(1\) if \(m = 1\) and \(0\) otherwise, and \(\Lambda(m) = \sum_{d \mid m} \mu(d) \, L(m/d)\), where both sums run over the \(d\) with \(0 \le d \le m\) and \(d \mid m\). Then for all natural numbers \(U \ge 1\), \(V \ge 1\) and \(n > V\),

\[\Lambda(n) = \sum_{b \mid n,\ b \le U} \mu(b) \, L(n/b) - \sum_{b \mid n,\ b \le U} \ \sum_{c \le V,\ bc \mid n} \mu(b) \, \Lambda(c) + \sum_{b \mid n,\ b > U} \ \sum_{c > V,\ bc \mid n} \mu(b) \, \Lambda(c),\]

where \(b\) and \(c\) range over \(0, 1, \dots, n\).

When \(R = \mathbb{R}\), \(\mu\) is the Möbius function, \(L = \log\) and \(\Lambda\) is the von Mangoldt function, the hypotheses hold and this is the classical Vaughan identity.

MetaMathlibExt.vaughan_identity · 15 lines

theorem vaughan_identity {R : Type*} [CommRing R]
    (μ Λ : ArithmeticFunction R) (logW : ℕ → R)
    (U V n : ℕ) (hU : 1 ≤ U) (hV : 1 ≤ V) (hn : V < n)
    (hLambda : ∀ m, Λ m =
      ∑ d ∈ (Finset.range (m + 1)).filter (fun d => d ∣ m), μ d * logW (m / d))
    (hMu : ∀ m, ∑ d ∈ (Finset.range (m + 1)).filter (fun d => d ∣ m), μ d =
      if m = 1 then 1 else 0) :
    Λ n = (∑ b ∈ (Finset.range (n + 1)).filter (fun b => b ∣ n ∧ b ≤ U),
        μ b * logW (n / b))
      - (∑ b ∈ (Finset.range (n + 1)).filter (fun b => b ∣ n ∧ b ≤ U),
          ∑ c ∈ (Finset.range (n + 1)).filter (fun c => c ≤ V ∧ b * c ∣ n),
            μ b * Λ c)
      + (∑ b ∈ (Finset.range (n + 1)).filter (fun b => b ∣ n ∧ U < b),
          ∑ c ∈ (Finset.range (n + 1)).filter (fun c => V < c ∧ b * c ∣ n),
            μ b * Λ c)

Sources

• https://en.wikipedia.org/wiki/Vaughan%27s_identity It follows from vaughan_identity_general; the hypotheses hU and hV are unused and keep the source's shape.

Uses 1

Proof usesVaughan's identity in a commutative ring

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.