(8.18), Dirichlet regime:
ProvedTaoFivePrimes.minor_arc_Linfty_dirichletEstimate (8.18) in the Dirichlet regime. This is the substantive regime of the bound: is far enough from the origin that the archimedean model is useless, but not so far that the crude kernel bound suffices,
with , , .
Why it holds, following the paper. Here one uses the trivial kernel bound and reduces to the pure exponential sum estimate
Dirichlet approximation writes with , so the upper bound on forces , and the lower bound forces . Theorem 1.3 then applies in one of three forms according to the size of relative to , each with room against the budget: the weakly minor case via refinement (1.12); the intermediate case via the main estimate (1.9), which the paper bounds by ; and the strongly minor case via refinement (1.10), which it bounds by . The paper notes explicitly that the weakly minor case fails if (1.9) or (1.11) is used in place of (1.12).
Inputs. Theorem 1.3 in the forms (1.9), (1.10) and (1.12), the Dirichlet approximation, and the trivial kernel bound. Published statements of the three Theorem 1.3 forms are available as exp_sum_estimate, exp_sum_estimate_small_q and exp_sum_estimate_large_q_unit.
Formalization note. S0, DK and T0 are those of the published arc-split module. The lower endpoint is the upper endpoint of the weakly major regime and the upper endpoint is the lower endpoint of the crude regime, so the three regimes cover exactly.
import Mathlib import Definitions.Def_TaoFivePrimes_ArcSplit open TaoFivePrimes
namespace TaoFivePrimes
theorem minor_arc_Linfty_dirichlet (x : ℕ)
(h1 : 87 * 10 ^ 35 ≤ x) (h2 : (x : ℝ) ≤ Real.exp 3100)
(α : AddCircle (1 : ℝ))
(hlo : 1000 * T0 / (4 * Real.pi * x) < ‖α‖)
(hhi : ‖α‖ < 32 / (4 * 10 ^ 14)) :
‖S0 x α‖ * ‖DK (4 * 10 ^ 14) α‖ ≤ 0.05 * x * ((4 * 10 ^ 14 / 3 : ℕ) : ℝ) / 1000 := by
sorry
end TaoFivePrimes