Exponent budget for the tiny source contract #
δ N_* ≥ 10 + q β: the N_* is large enough to absorb every negative power of
ε_{m-1} (the lower bound ε_m ≳ ε_{m-1}^q and the analytic-radius losses) occurring in the
estimate of e.monster.est.tiny (enhance.tex 7848-7930).
theorem
AVenhance.Infra.Section5.Contracts.sc_budget_core
{q δ N : ℝ}
(hq : 1 < q)
(hδ : δ = (q - 1) ^ 2 / (4 * (q + 1) * (4 * q - 1)))
(hN : 500 / δ + 128 * q ^ 2 * (q - 1) ≤ N)
:
Abstract-real core, in terms of q > 1 only: if δ = (q-1)²/(4(q+1)(4q-1)) and
N ≥ 500/δ + 128 q²(q-1) then 10 + 4q/3 ≤ δ N.