Fourier coefficient of the cube of a weighted exponential sum

Proved

Vino.integral_cube_orthogonality

by tabbott · Sep 2, 2026 · Mathlib c5ea003 (Lean v4.30.0)

analytic-number-theorycircle-methodnumber-theoryprime-numbers

Let $w:\mathbb N\to\mathbb C$ be arbitrary weights and set $F(\alpha)=\sum_{a<N}w(a)e(\alpha a)$ . Then for every natural number $n$ ,

\int_0^1 F(\alpha)^3\,e(-n\alpha)\,d\alpha\;=\;\sum_{\substack{a,b,c<N\\ a+b+c=n}}w(a)w(b)w(c).

This is the fundamental counting identity of the circle method in its ternary, weighted form: the $n$ -th Fourier coefficient of $F^3$ is the weighted number of representations of $n$ as an ordered sum of three elements below $N$ . Stating it for arbitrary weights rather than for a specific arithmetic function is what makes it reusable — the von Mangoldt weighting, the indicator of the primes and any smoothed variant are all instances.

Preamble

import Definitions.Def_CircleMethod_char
import Mathlib.Analysis.SpecialFunctions.Integrals.Basic
open Finset

Formal statement

namespace Vino

theorem integral_cube_orthogonality (w : ℕ → ℂ) (N : ℕ) (n : ℕ) :
    (∫ α in (0:ℝ)..1,
        (∑ a ∈ Finset.range N, w a * CircleMethod.e (α * (a : ℝ))) ^ 3
          * CircleMethod.e (-(n : ℝ) * α))
      = ∑ a ∈ Finset.range N, ∑ b ∈ Finset.range N, ∑ c ∈ Finset.range N,
          if a + b + c = n then w a * w b * w c else 0 := by sorry

end Vino

Source

R. C. Vaughan, The Hardy-Littlewood Method, 2nd ed., Cambridge Tracts in Mathematics 125, Cambridge University Press, 1997, Section 1.1 equation (1.4) (the fundamental counting identity of the circle method) and Chapter 3 (the three primes theorem).

View graph