Fourier identity for Tao’s weighted representation count (equation 8.11)
ProvedTaoFivePrimes.representationCount_fouriercircle-methodfourier-analysisgoldbachnumber-theory
For every pair of natural numbers x and H, the finite circle-method integrand is integrable, and its integral over the unit circle is exactly the weighted representation count R(x,H), viewed as a complex number. Each positive shift runs from 1 through floor(H/3). The third prime sum uses K=1000. This is the finite-sum form of equation (8.11), obtained by Fourier orthogonality. It holds without any analytic estimates or lower bound on x. In particular, the result does not assert that the count is positive.
Preamble
import Definitions.Def_TaoFivePrimes_FourierRepresentation open MeasureTheory
Formal statement
theorem TaoFivePrimes.representationCount_fourier (x H : ℕ) :
Integrable (TaoFivePrimes.representationIntegrand x H) AddCircle.haarAddCircle ∧
(TaoFivePrimes.representationCount x H : ℂ) =
∫ α : AddCircle (1 : ℝ), TaoFivePrimes.representationIntegrand x H α
∂AddCircle.haarAddCircle := by sorrySource
Terence Tao, https://arxiv.org/abs/1201.6656, Section8, equation(8.11) and the choice K=1000 immediately following it. Finite Fourier coefficient extraction for the count in equation(8.10).