Coefficient control on the integer grid in every finite dimension. Iterating the sharp univariate bound gives the factor 3^(nd) over ℂ (CCDN Lemma 3.4.2); the real and integer statements, with the weaker factor (d+1)^(n(d+1)), are corollaries obtained by embedding the coefficients in ℂ.

theorem CCDN.exists_complex_multivariate_grid_height_witness {n : ℕ} (f : MvPolynomial (Fin n) ℂ) {d : ℕ} (hd : f.totalDegree ≤ d) : ∃ (a : Fin n → ℕ), (∀ (i : Fin n), a i ≤ d) ∧ ∀ (m : Fin n →₀ ℕ), ‖f.coeff m‖ ≤ 3 ^ (n * d) * ‖(MvPolynomial.eval fun (i : Fin n) => ↑(a i)) f‖

A complex polynomial of total degree at most d has a grid point a ∈ [0, d]ⁿ at which its value bounds every coefficient: ‖coeff m‖ ≤ 3^(n d) ‖f(a)‖.

theorem CCDN.multivariate_coefficient_bound_of_integer_grid {n : ℕ} (f : MvPolynomial (Fin n) ℝ) {d : ℕ} (hd : f.totalDegree ≤ d) {H : ℝ} (hH : 0 ≤ H) (heval : ∀ (a : Fin n → ℕ), (∀ (i : Fin n), a i ≤ d) → |(MvPolynomial.eval fun (i : Fin n) => ↑(a i)) f| ≤ H) (m : Fin n →₀ ℕ) : |f.coeff m| ≤ (↑d + 1) ^ (n * (d + 1)) * H

Iterated one-variable interpolation controls every coefficient from the values on the full grid, with a constant depending only on degree and dimension.

theorem CCDN.integer_multivariate_coefficient_bound_of_grid {n : ℕ} (f : MvPolynomial (Fin n) ℤ) {d : ℕ} (hd : f.totalDegree ≤ d) {H : ℝ} (hH : 0 ≤ H) (heval : ∀ (a : Fin n → ℕ), (∀ (i : Fin n), a i ≤ d) → |↑((MvPolynomial.eval fun (i : Fin n) => ↑(a i)) f)| ≤ H) (m : Fin n →₀ ℕ) : |↑(f.coeff m)| ≤ (↑d + 1) ^ (n * (d + 1)) * H

If an integer polynomial of total degree at most d has values of absolute value at most H on the grid {0, …, d}ⁿ, then every coefficient has absolute value at most (d + 1) ^ (n * (d + 1)) * H.

theorem CCDN.exists_integer_multivariate_grid_height_witness {n : ℕ} (f : MvPolynomial (Fin n) ℤ) (hf : f ≠ 0) {d : ℕ} (hd : f.totalDegree ≤ d) : ∃ (a : Fin n → ℤ), (∀ (i : Fin n), 0 ≤ a i ∧ a i ≤ ↑d) ∧ (MvPolynomial.eval a) f ≠ 0 ∧ ∀ (m : Fin n →₀ ℕ), |↑(f.coeff m)| ≤ (↑d + 1) ^ (n * (d + 1)) * |↑((MvPolynomial.eval a) f)|

A nonzero integer polynomial of total degree at most d has a point a of the grid {0, …, d}ⁿ with f(a) ≠ 0 such that every coefficient has absolute value at most (d + 1) ^ (n * (d + 1)) * |f(a)|.