Integral evaluation and coefficient-uniform height control for the two moment coordinates in the degree-preserving projection.

Evaluation of the moment coordinates used by the bounded primitive pair.

theorem CCDN.momentCoordinate_eval {K : Type u_1} [CommRing K] {n : ℕ} (k : ℕ) (z : Fin n → K) : (MvPolynomial.eval z) (momentCoordinate K n k) = ∑ j : Fin n, ↑k ^ ↑j * z j

Evaluating the moment coordinate with parameter k at z gives ∑ j, k ^ j * z j.

noncomputable def CCDN.degreeProjection (n k₀ k₁ : ℕ) (z : IntPoint n) : IntPoint 2

The integer projection of ℤⁿ to ℤ² given by the two moment coordinates with parameters k₀ and k₁.

Equations

• CCDN.degreeProjection n k₀ k₁ z = ![(MvPolynomial.eval z) (CCDN.momentCoordinate ℤ n k₀), (MvPolynomial.eval z) (CCDN.momentCoordinate ℤ n k₁)]

def CCDN.projectionBoxFactor (n d : ℕ) : ℝ

The box scaling factor (n + 1) * ((n + 1) * (d + 1)) ^ (2 * n) for the moment projection in n variables and degree d.

Equations

• CCDN.projectionBoxFactor n d = (↑n + 1) * (((↑n + 1) * (↑d + 1)) ^ 2) ^ n

theorem CCDN.projectionBoxFactor_one_le (n d : ℕ) : 1 ≤ projectionBoxFactor n d

The box scaling factor of the moment projection is at least one.

theorem CCDN.degreeProjection_box {n d k₀ k₁ : ℕ} (hk₀ : k₀ ≤ n ^ 2 * d) (hk₁ : k₁ ≤ n * d ^ 2) {B : ℝ} (hB : 0 ≤ B) {z : IntPoint n} (hz : z ∈ integerBox n B) : degreeProjection n k₀ k₁ z ∈ integerBox 2 (projectionBoxFactor n d * B)

For parameters k₀ ≤ n ^ 2 * d and k₁ ≤ n * d ^ 2, the moment projection maps the integer box of radius B into the integer box of radius projectionBoxFactor n d * B.

theorem CCDN.rationalPoint_moment_eval {n : ℕ} (k : ℕ) (z : IntPoint n) : ↑((MvPolynomial.eval z) (momentCoordinate ℤ n k)) = (MvPolynomial.eval (rationalPoint z)) (momentCoordinate ℚ n k)

Evaluating the integer moment coordinate at an integer point and casting to ℚ agrees with evaluating the rational moment coordinate at the corresponding rational point.

theorem CCDN.rationalPoint_degreeProjection {n k₀ k₁ : ℕ} (z : IntPoint n) : rationalPoint (degreeProjection n k₀ k₁ z) = ![(MvPolynomial.eval (rationalPoint z)) (momentCoordinate ℚ n k₀), (MvPolynomial.eval (rationalPoint z)) (momentCoordinate ℚ n k₁)]

The rational point of the integer moment projection of z is the pair of rational moment coordinates evaluated at z.