Power bounds for values under the height hypothesis

theorem NairTenenbaum.eval_natAbs_le_height_real (Q : Polynomial ℤ) {x : ℝ} (hx : 1 ≤ x) {n : ℤ} (hn : ↑n.natAbs ≤ 2 * x) : ↑(Polynomial.eval n Q).natAbs ≤ ↑(polynomialHeight Q) * (↑Q.natDegree + 1) * (2 * x) ^ Q.natDegree

theorem NairTenenbaum.eval_natAbs_le_rpow_of_height {Q : Polynomial ℤ} {g : ℕ} (hg : Q.natDegree = g) {x δ : ℝ} (hx : 1 ≤ x) (hδ : 0 < δ) (hheight : ↑(polynomialHeight Q) ^ δ ≤ x) (hlarge : (↑g + 1) * 2 ^ g ≤ x) {n : ℤ} (hn : ↑n.natAbs ≤ 2 * x) : ↑(Polynomial.eval n Q).natAbs ≤ x ^ (↑g + 1 / δ + 1)

A uniform threshold absorbs the elementary coefficient-height constant. The exponent has one unit of slack, avoiding any coefficient-dependent constant.

theorem NairTenenbaum.eval_natAbs_le_const_rpow_of_height {Q : Polynomial ℤ} {g : ℕ} (hg : Q.natDegree = g) {x δ : ℝ} (hx : 1 ≤ x) (hδ : 0 < δ) (hheight : ↑(polynomialHeight Q) ^ δ ≤ x) {n : ℤ} (hn : ↑n.natAbs ≤ 2 * x) : ↑(Polynomial.eval n Q).natAbs ≤ (↑g + 1) * 2 ^ g * x ^ (↑g + 1 / δ)

Retaining the degree-only coefficient avoids losing a power of x when bounding contributions that rely on a small positive exponent saving.