A coefficient-height witness on the bounded integer plane grid: the case n = 2 of
CCDN.Height.MultivariateGridHeight.
theorem
CCDN.bivariatePolynomialEquiv_eval
{R : Type u_1}
[CommRing R]
(f : MvPolynomial (Fin 2) R)
(x y : R)
:
Polynomial.eval x (Polynomial.map (Polynomial.evalRingHom y) ((bivariatePolynomialEquiv R) f)) = (MvPolynomial.eval ![x, y]) f
Evaluating the nested-polynomial form of a bivariate polynomial f at (x, y) (inner
variable at y, outer variable at x) agrees with evaluating f at ![x, y].
theorem
CCDN.bivariate_coefficient_bound_of_integer_grid
(f : Polynomial (Polynomial ℝ))
{d : ℕ}
(hd : bivariateTotalDegree f ≤ d)
{H : ℝ}
(hH : 0 ≤ H)
(heval : ∀ (x y : ℕ), x ≤ d → y ≤ d → |Polynomial.eval (↑x) (Polynomial.map (Polynomial.evalRingHom ↑y) f)| ≤ H)
(i j : ℕ)
:
The plane case of multivariate_coefficient_bound_of_integer_grid, for nested
polynomials.
theorem
CCDN.exists_integer_plane_grid_height_witness
(f : MvPolynomial (Fin 2) ℤ)
(hf : f ≠ 0)
{d : ℕ}
(hd : f.totalDegree ≤ d)
:
A nonzero integer plane polynomial of total degree at most d has a nonzero value at some
natural point (x, y) with x, y ≤ d, and every coefficient is bounded by
(d + 1) ^ (2 * (d + 1)) times the absolute value of that value.