Coefficient-height bounds for evaluating a polynomial on a bounded box. The constants depend only on total degree and the number of variables.

theorem CCDN.polynomial_eval₂_box_bound {σ : Type u_1} [Fintype σ] (f : MvPolynomial σ ℤ) (H A : ℝ) (hH : 0 ≤ H) (hA : 1 ≤ A) (hf : CoefficientHeightLE f H) (v : σ → ℝ) (hv : ∀ (i : σ), |v i| ≤ A) : |MvPolynomial.eval₂ (Int.castRingHom ℝ) v f| ≤ (↑f.totalDegree + 1) ^ Fintype.card σ * H * A ^ f.totalDegree

An evaluation estimate with no coefficient-dependent constants.