HighFreqBandEstimate

Slow factor and factorization

Pointwise bounds

Interval partition quantities

Infrastructure: Haar-to-interval decomposition

The key identity relating Haar integrals on AddCircle T to interval integrals on ℝ is:

∫ f ∂haarAddCircle = (1/T) ∑_{k=0}^{N-1} ∫_{I_k} f(↑t) dt

This follows from:

• AddCircle.integral_preimage: ∫ₜ∈Ioc(0,T) f(↑t) dt = ∫ f ∂volume
• AddCircle.volume_eq_smul_haarAddCircle: volume = T • haarAddCircle
• Additivity of interval integrals.

Intermediate lemmas (4.1a–d)

Parseval identity for finite Fourier sums indexed by Fin L

Auxiliary

Core lower bound

Combines assembly + Poincaré to get: ∫ ρ(P)² d(haar) ≥ circleNormSq(Q) / 32.

The arithmetic reduces to: 136π²(L−1)² ≤ N² (under 1343L² ≤ N²).

Since 136π² ≈ 1342.27, we need ⌈136π²⌉ = 1343. The hypothesis 1343 * L^2 ≤ N^2 implies 136π²(L-1)² ≤ 136π²L² ≤ 1343L² ≤ N².

Main theorem

theorem FockSPR.high_freq_band_estimate {N L : ℕ} (hN : 1 ≤ N) (hL : 1 ≤ L) (hNL : 1343 * L ^ 2 ≤ N ^ 2) (b : Fin L → ℂ) (P : AddCircle T → ℂ) (hP : P = fun (t : AddCircle T) => ∑ m : Fin L, b m * (fourier ↑(N + ↑m)) t) : circleNormSq P ≤ 32 * ∫ (t : AddCircle T), rho (P t) ^ 2 ∂AddCircle.haarAddCircle

Theorem 4.1: High-frequency band estimate. For N ≥ 1, L ≥ 1, 1343·L² ≤ N², and P(t) = ∑ b(m)·fourier(N+m)(t): circleNormSq(P) ≤ 32 · ∫ ρ(P)² d(haar).