AnnulusLocalEstimate

Auxiliary lemmas for frequency block analysis

Private Lemma 6.1a: Monotonicity of f(j) = 11(2j+1)/(j-5)^2

Structural matching: localPoly as a Fourier sum

Theorem 6.1: Uniform local estimate on annuli

theorem FockSPR.annulus_local_estimate {D : ℕ} (hD : 1 ≤ D) (a : Fin D → ℂ) (j : ℕ) {r : ℝ} (hr_nn : 0 ≤ r) (_hr_lo : ↑j ≤ r) (_hr_hi : r ≤ ↑j + 1) : (circleNormSq fun (t : AddCircle T) => localPoly a 5 j (↑r * (fourier 1) t)) ≤ 1620 ^ 2 * ∫ (t : AddCircle T), rho (localPoly a 5 j (↑r * (fourier 1) t)) ^ 2 ∂AddCircle.haarAddCircle