Vaughan's identity in the Type I interface vocabulary

Proved

TaoFivePrimes.vaughan_identity_interface

by andreaskapfer · Sep 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

exponential-sumsfive-primesnumber-theoryvaughan-identity

Vaughan's identity in the interface vocabulary

For integers $U,V\ge0$ , the platform's restricted Möbius and von Mangoldt functions satisfy

\mu_{\le U}*\log-\mu_{\le U}*\Lambda_{\le V}*\zeta+\mu_{>U}*\Lambda_{>V}*\zeta+\Lambda_{\le V}=\Lambda .

This is Vaughan's identity in the form used by Tao's Lemma 4.11 in the arithmeticRestrictLE/arithmeticRestrictGT vocabulary of the Type I interface: the first three terms are exactly the Type I part vaughanTypeIPart with its third term written as $\mu_{>U}*(\Lambda_{>V}*\zeta)$ instead of the centred half-logarithm $\mu_{>U}*(\tfrac12\log)_{>V}$ , and the closing term $\Lambda_{\le V}$ is invisible against any test function supported above $V$ .

The proof is the standard one: $\log=\Lambda*\zeta$ and $\mu*\zeta=1$ , so $\Lambda=\mu*\log$ ; splitting $\mu=\mu_{\le U}+\mu_{>U}$ and $\Lambda=\Lambda_{\le V}+\Lambda_{>V}$ and rearranging the Dirichlet products gives the identity.

Preamble

import Mathlib
import Theorems.Thm_TaoFivePrimes_typeIExpansion_three_bilinear_sums

open scoped ArithmeticFunction.vonMangoldt ArithmeticFunction.Moebius BigOperators
open ArithmeticFunction Finset

Formal statement

theorem TaoFivePrimes.vaughan_identity_interface (U V : ℕ) :
    TaoFivePrimes.arithmeticRestrictLE U (μ : ArithmeticFunction ℝ) * ArithmeticFunction.log
      - TaoFivePrimes.arithmeticRestrictLE U (μ : ArithmeticFunction ℝ) *
          TaoFivePrimes.arithmeticRestrictLE V ArithmeticFunction.vonMangoldt *
          (ArithmeticFunction.zeta : ArithmeticFunction ℝ)
      + TaoFivePrimes.arithmeticRestrictGT U (μ : ArithmeticFunction ℝ) *
          TaoFivePrimes.arithmeticRestrictGT V ArithmeticFunction.vonMangoldt *
          (ArithmeticFunction.zeta : ArithmeticFunction ℝ)
      + TaoFivePrimes.arithmeticRestrictLE V ArithmeticFunction.vonMangoldt
      = ArithmeticFunction.vonMangoldt := by sorry

Source

Terence Tao, arXiv:1201.6656v4, Lemma 4.11 (Vaughan's identity), in the restricted-arithmetic-function vocabulary of Definition TaoFivePrimes_TypeIEnvelopeInterfaces.

View graph