Power savings with the growth margin of Theorem 3

The admissibility exponent εδ/3 leaves a smaller positive gap than the progression bound requires. Keeping that gap explicit avoids strengthening the hypotheses on the arithmetic function.

theorem NairTenenbaum.PolynomialSystem.primePowerContribution_primeArgument_power_saving {k r g : ℕ} (P : PolynomialSystem k r) (hdeg : P.total.natDegree = g) {A B σ ε c x y : ℝ} {F : ArithmeticMap k} (hF : Admissible A B σ F) (hB : 0 ≤ B) (hσ : 0 ≤ σ) (hε : 0 ≤ ε) (hx : 1 ≤ x) (hmargin : c * σ ≤ 17 * ↑g * ε / 24) {a b : ℤ} (hab : a ≤ b) (hlevel : (x ^ (↑g * ε / 2)) ^ 4 ≤ ↑b - ↑a) (hlen : ↑b - ↑a ≤ 2 * y) (hvalue : ∀ t ∈ Finset.Ioc a b, ↑(Polynomial.eval t P.total).natAbs ≤ x ^ c) : P.primePowerContribution F (x ^ (↑g * ε / 2)) a b ≤ 8 * ↑g * ↑(max g (P.badDiscriminant ^ 3)) * B * y * x ^ (-(↑g * ε / 24)) * F 1

theorem NairTenenbaum.PolynomialSystem.smoothDivisorContribution_primeArgument_power_saving {k r g : ℕ} (P : PolynomialSystem k r) (hdeg : P.total.natDegree = g) {A B σ ε c x y : ℝ} {F : ArithmeticMap k} (hF : Admissible A B σ F) (hB : 0 ≤ B) (hσ : 0 ≤ σ) (hx : 1 ≤ x) (hmargin : c * σ ≤ 17 * ↑g * ε / 24) (s : Finset ℕ) (N : ℕ+) {a b : ℤ} (hab : a ≤ b) (hlevel : ↑↑N ≤ ↑b - ↑a) (hlen : ↑b - ↑a ≤ 2 * y) (hvalue : ∀ t ∈ Finset.Ioc a b, ↑(Polynomial.eval t P.total).natAbs ≤ x ^ c) : P.smoothDivisorContribution F s N (x ^ (3 * ↑g * ε / 2)) a b ≤ 4 * smoothDivisorBound g P.badDiscriminant s * B * y * x ^ (-(↑g * ε / 24)) * F 1

The same growth margin pays the smooth-divisor saving.