LocalCircleEstimate

Theorem 3.1: Quantitative local estimate on S¹

Utility lemmas

Fourier orthogonality

Parseval identity for finite Fourier sums

Private Lemma 3.1a: L∞ bound

∫ P² = 0 for positive-frequency sums

Private Lemma 3.1b: Equal L² masses

Pointwise bound: rho(w)² ≥ w.re²/2 - ‖w‖⁴

∫ ‖P‖⁴ bound

Private Lemma 3.1c: Small-amplitude regime

∫ ‖1+P‖² = 1 + circleNormSq P

Integral Cauchy-Schwarz for real-valued functions

Private Lemma 3.1d: Large-amplitude regime

Theorem 3.1 (Main statement)

theorem FockSPR.local_circle_estimate {L : ℕ} (hL : 1 ≤ L) {E : Finset ℕ} (hE : E.card = L) (hE_pos : ∀ n ∈ E, 1 ≤ n) (b : ℕ → ℂ) (P : AddCircle T → ℂ) (hP : P = fun (t : AddCircle T) => ∑ n ∈ E, b n * (fourier ↑n) t) : circleNormSq P ≤ 144 * ↑L * ∫ (t : AddCircle T), rho (P t) ^ 2 ∂AddCircle.haarAddCircle