Lemma U: the final cutoff optimisation #
Abstract real arithmetic. Given the low/high Fourier split bound
X ≤ S² (h (80 κ K² + B²/κ) + 1/(9K²) + B²/(36 κ² K²)) for every integer cutoff K ≥ 1, the
choice K = ⌈h^{-1/4} κ^{-3/4}⌉ gives √X ≤ 20 (1+B) κ^{-1/2} h^{1/4} S.
theorem
AVenhance.Infra.FullTheorem.LemmaU.optimize_core
{u v B S X K : ℝ}
(hu0 : 0 < u)
(hu1 : u ≤ 1)
(hv0 : 0 < v)
(hv1 : v ≤ 1)
(hB : 0 ≤ B)
(hKx : 1 / (u * v ^ 3) ≤ K)
(hK2 : K ≤ 2 / (u * v ^ 3))
(hX : X ≤ S ^ 2 * (u ^ 4 * (80 * v ^ 4 * K ^ 2 + B ^ 2 / v ^ 4) + 1 / (9 * K ^ 2) + B ^ 2 / (36 * (v ^ 4) ^ 2 * K ^ 2)))
:
Core inequality in the variables u = h^{1/4}, v = κ^{1/4}.
theorem
AVenhance.Infra.FullTheorem.LemmaU.lemmaU_optimize
{h κ B S X : ℝ}
(hh : 0 < h)
(hh1 : h ≤ 1)
(hκ : 0 < κ)
(hκ1 : κ ≤ 1)
(hB : 0 ≤ B)
(hS : 0 ≤ S)
(hX :
∀ (K : ℕ), 1 ≤ K → X ≤ S ^ 2 * (h * (80 * κ * ↑K ^ 2 + B ^ 2 / κ) + 1 / (9 * ↑K ^ 2) + B ^ 2 / (36 * κ ^ 2 * ↑K ^ 2)))
:
The final square-root optimisation of Lemma U.