Parseval: $\int_0^1 |S(\alpha,N)|^2 d\alpha = \sum_{n<N} \Lambda(n)^2$

Proved

Vino.parseval

by jjosh · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

circle-methodnumber-theoryparsevalprimes

For the von Mangoldt exponential sum $S(\alpha,N)=\sum_{n<N}\Lambda(n)e(\alpha n)$ , its squared $L^2$ norm over the circle equals $\sum_{n<N}\Lambda(n)^2$ :

\int_0^1 |S(\alpha,N)|^2\,d\alpha = \sum_{n<N}\Lambda(n)^2.

This is the diagonal-extraction identity (orthogonality applied to $S\cdot\overline{S}$ ) that underlies all minor-arc $L^2$ control in the circle method: it is exactly why $\int_{\mathfrak m}|S|^2 \ll N\log N$ , and equally why $L^2$ control alone cannot isolate the binary Goldbach main term.

Preamble

import Mathlib
import Definitions.Def_Vino_primes
import Definitions.Def_CircleMethod_char

Formal statement

namespace Vino

theorem parseval (N : ℕ) :
    (∫ α in (0:ℝ)..1, (Vino.vmSum α N) * star (Vino.vmSum α N))
      = ∑ a ∈ Finset.range N,
          (((ArithmeticFunction.vonMangoldt a : ℝ) : ℂ)) ^ 2 := by
  sorry

end Vino

Source

standard; e.g. Montgomery--Vaughan, Multiplicative Number Theory I

View graph

Parseval: ∫01∣S(α,N)∣2dα=∑n<NΛ(n)2\int_0^1 |S(\alpha,N)|^2 d\alpha = \sum_{n<N} \Lambda(n)^2∫01​∣S(α,N)∣2dα=∑n<N​Λ(n)2

Parseval: $\int_0^1 |S(\alpha,N)|^2 d\alpha = \sum_{n<N} \Lambda(n)^2$