Tao Prop 4.8 tail estimate: L1 mass of the eta-Fourier series away from the origin
ProvedTaoFivePrimes.fourier_tail_L1_boundLet be smooth and compactly supported, let , and set
Then for every ,
where is the distance from to the nearest integer and is the second derivative of . The region of integration is a fundamental domain for , namely the union of the two intervals and .
This estimate is the step in the proof of Proposition 4.8 that controls the contribution of the frequencies lying outside the major arc; it is what makes the lower bound of that proposition sharp, to within a factor of two, against the upper bound of Corollary 4.7 when is not too large.
Fidelity note The source states this step with , which equals , in place of . The function occurring in the Parseval identity of that same proof is built from rather than , and the constant stated here is the one the argument produces. The two differ only in which cutoff is differentiated, so the later applications go through after the corresponding substitution.
Formalization Note The series defining is an unconditional sum over , convergent because compact support leaves only finitely many nonzero terms.
import Mathlib import Definitions.Def_TaoFivePrimes_Explicit open MeasureTheory
theorem TaoFivePrimes.fourier_tail_L1_bound
(eta : ℝ → ℝ) (hsm : ContDiff ℝ (⊤ : ℕ∞) eta) (hc : HasCompactSupport eta)
(x : ℝ) (hx : 0 < x) (r : ℝ) (hr0 : 0 < r) (hr : r < 1 / 2) :
(∫ theta in (-(1/2) : ℝ)..(-r),
‖∑' n : ℤ, ((eta ((n : ℝ) / x) : ℝ) : ℂ) * TaoFivePrimes.eR (theta * n)‖)
+ (∫ theta in r..(1/2 : ℝ),
‖∑' n : ℤ, ((eta ((n : ℝ) / x) : ℝ) : ℂ) * TaoFivePrimes.eR (theta * n)‖)
≤ (∫ t : ℝ, |iteratedDeriv 2 eta t|) / (2 * Real.pi ^ 2 * r * x) := by sorry