Prove2Me

Quantitative Parseval bound ∫01∣S∣2≤Nlog⁡2N\int_0^1 |S|^2 \le N\log^2 N

Proved
Vino.parseval_le

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

circle-methodnumber-theoryparsevalprimes

For the von Mangoldt exponential sum S(α,N)=∑n<NΛ(n)e(αn)S(\alpha,N)=\sum_{n<N}\Lambda(n)e(\alpha n),

∫01∣S(α,N)∣2 dα≤N (log⁡N)2.\int_0^1 |S(\alpha,N)|^2\,d\alpha \le N\,(\log N)^2.

This follows from the proved diagonal identity Vino.parseval, ∫∣S∣2=∑n<NΛ(n)2\int|S|^2 = \sum_{n<N}\Lambda(n)^2, and the elementary bound Λ(n)≤log⁡n\Lambda(n)\le\log n. It is the sharp quantitative form of the trivial-weight L2L^2 bound: with a factor log⁡N\log N it controls the minor-arc mass in the ternary problem, while in the binary problem ∫∣S∣2\int|S|^2 alone cannot separate the main term S⋅m\mathfrak S\cdot m — the analytic content of the parity barrier.

Preamble
import Mathlib
import Definitions.Def_Vino_primes
import Definitions.Def_CircleMethod_char
import Theorems.Thm_Vino_parseval
Formal statement
namespace Vino

theorem parseval_le (N : ℕ) (hN : 1 ≤ N) :
    ‖∫ α in (0:ℝ)..1, (Vino.vmSum α N) * star (Vino.vmSum α N)‖
      ≤ (N : ℝ) * Real.log N ^ 2 := by
  sorry

end Vino
Source
standard corollary of Parseval + Λ≤log⁡\Lambda\le\log

View graph