AnalyticNumberTheory.Sieve.VaughanIdentity

Vaughan's identity

Vaughan (1977) decomposes the von Mangoldt function as

Λ(n) = Σ_{d|n, d≤u} μ(d) log(n/d) + Σ_{d|n, u<d} Σ_{e|n/d, e≤v} μ(d) Λ(e) + Σ_{d|n, u<d} Σ_{e|n/d, v<e} μ(d) Λ(e).

This is a structural bridge in the Bombieri--Vinogradov and weighted Pan mean-value arguments (PanMeanValueUniform). The first term is Type I, a convolution of truncated μ with log; the third is Type II, bilinear in two truncated factors. The middle term is reorganized by Moebius inversion.

This module treats only exact finite algebra, with no analytic estimates. The first identity holds for all n,u,v. Starting from mathlib's ArithmeticFunction.moebius_mul_log_eq_vonMangoldt (μ * log = Λ), split the convolution at d ≤ u / u < d, then at e ≤ v / v < e.

References:

• Vaughan, R.C. (1977), Acta Arith. 32, 125-142
• Halberstam & Richert, "Sieve Methods" (1974), Ch. 9-10
• Iwaniec & Kowalski, "Analytic Number Theory" (2004), Ch. 13.4

1. Truncated terms

noncomputable def AnalyticNumberTheory.Sieve.vaughanFirst (n u : ℕ) : ℝ

Type I main term: Σ_{d|n, d≤u} μ(d) log(n/d).

Equations

• AnalyticNumberTheory.Sieve.vaughanFirst n u = ∑ d ∈ n.divisors with d ≤ u, ↑(ArithmeticFunction.moebius d) * Real.log ↑(n / d)

noncomputable def AnalyticNumberTheory.Sieve.vaughanSecond (n u v : ℕ) : ℝ

Intermediate term (Type I'): Σ_{d|n, u<d} Σ_{e|n/d, e≤v} μ(d) Λ(e).

Equations

• AnalyticNumberTheory.Sieve.vaughanSecond n u v = ∑ d ∈ n.divisors with u < d, ∑ e ∈ (n / d).divisors with e ≤ v, ↑(ArithmeticFunction.moebius d) * ArithmeticFunction.vonMangoldt e

noncomputable def AnalyticNumberTheory.Sieve.vaughanThird (n u v : ℕ) : ℝ

Type II bilinear term: Σ_{d|n, u<d} Σ_{e|n/d, v<e} μ(d) Λ(e).

Equations

• AnalyticNumberTheory.Sieve.vaughanThird n u v = ∑ d ∈ n.divisors with u < d, ∑ e ∈ (n / d).divisors with v < e, ↑(ArithmeticFunction.moebius d) * ArithmeticFunction.vonMangoldt e

noncomputable def AnalyticNumberTheory.Sieve.vaughanMiddle (n u v : ℕ) : ℝ

Middle term in the classical three-term form (Type I'): Σ_{d|n, d≤u} Σ_{e|n/d, e≤v} μ(d) Λ(e).

Equations

• AnalyticNumberTheory.Sieve.vaughanMiddle n u v = ∑ d ∈ n.divisors with d ≤ u, ∑ e ∈ (n / d).divisors with e ≤ v, ↑(ArithmeticFunction.moebius d) * ArithmeticFunction.vonMangoldt e

2. Exact three-part identity

theorem AnalyticNumberTheory.Sieve.vaughanIdentity (n u v : ℕ) : ArithmeticFunction.vonMangoldt n = vaughanFirst n u + vaughanSecond n u v + vaughanThird n u v

Vaughan's identity, exact form: for any n u v : ℕ, Λ n = vaughanFirst n u + vaughanSecond n u v + vaughanThird n u v. No hypotheses n > u or n > v are needed; this is finite convolution algebra.

3. Classical three-term form for n > v

theorem AnalyticNumberTheory.Sieve.moebiusDivisorSum_eq_ite (m : ℕ) : ∑ d ∈ m.divisors, ↑(ArithmeticFunction.moebius d) = if m = 1 then 1 else 0

Moebius divisor sum: Σ_{d|m} μ(d) = [m=1], from μ * ζ = 1 (the convolution unit) and coe_mul_zeta_apply.

theorem AnalyticNumberTheory.Sieve.vaughanDoubleSum_swap (n v : ℕ) : ∑ d ∈ n.divisors, ∑ e ∈ (n / d).divisors with e ≤ v, ↑(ArithmeticFunction.moebius d) * ArithmeticFunction.vonMangoldt e = ∑ e ∈ n.divisors with e ≤ v, ArithmeticFunction.vonMangoldt e * ∑ d ∈ (n / e).divisors, ↑(ArithmeticFunction.moebius d)

Exchange of Vaughan's double sum: rewrite Σ_{d|n} Σ_{e|n/d, e≤v} μ(d)Λ(e) as Σ_{e|n, e≤v} Λ(e)·Σ_{d|n/e} μ(d) by swapping the finite divisibility-indexed pairs (d,e).

theorem AnalyticNumberTheory.Sieve.vaughanFullSecondSum (n v : ℕ) : ∑ d ∈ n.divisors, ∑ e ∈ (n / d).divisors with e ≤ v, ↑(ArithmeticFunction.moebius d) * ArithmeticFunction.vonMangoldt e = if n ≤ v then ArithmeticFunction.vonMangoldt n else 0

Full second-level sum: Σ_{d|n} Σ_{e|n/d, e≤v} μ(d)Λ(e) = Λ(n)·[n≤v].

theorem AnalyticNumberTheory.Sieve.vaughanIdentity_threeTerm (n u v : ℕ) (hnv : v < n) : ArithmeticFunction.vonMangoldt n = vaughanFirst n u - vaughanMiddle n u v + vaughanThird n u v

Vaughan's identity, classical three-term form: for n > v, Λ n = vaughanFirst n u − vaughanMiddle n u v + vaughanThird n u v. This is the Type I/II form used in Bombieri--Vinogradov and weighted Pan arguments. By vaughanFullSecondSum, the middle and second terms cancel because Σ_{d|n} Σ_{e|n/d,e≤v} μ(d)Λ(e) = 0 when n > v.