The bounded leading-coefficient translation has a controlled height cost. Its logarithmic coefficient-position loss is at most 14d².

Coefficient height controls homogeneous evaluations, uniformly on the integer point box, with the exact number of monomials.

def CCDN.leadingPositionHeightFactor (d : ℕ) : ℝ

The height-loss factor (d + 1) ^ (4 (d + 1)) (d + 2) ^ 2 (2 d + 1) ^ d by which the coefficients of the affine chart of a ternary form of degree d, after a translation with parameters in [0, d], may exceed a coefficient height L of the form (measured as (d + 1) ^ (2 (d + 1)) * L); see homogeneousTranslation_chart_coefficient_bound.

Equations

• CCDN.leadingPositionHeightFactor d = (↑d + 1) ^ (4 * (d + 1)) * (↑d + 2) ^ 2 * (2 * ↑d + 1) ^ d

theorem CCDN.leadingPositionHeightFactor_one_le (d : ℕ) : 1 ≤ leadingPositionHeightFactor d

The factor leadingPositionHeightFactor d is at least 1.

theorem CCDN.leadingPositionHeightFactor_log_le {d : ℕ} (hd : 0 < d) : Real.log (leadingPositionHeightFactor d) ≤ 14 * ↑d ^ 2

For d ≥ 1, the logarithm of leadingPositionHeightFactor d is at most 14 d².

theorem CCDN.homogeneousTranslation_chart_coefficient_bound {d : ℕ} (f : MvPolynomial (Fin 3) ℤ) (hf : f.IsHomogeneous d) (a : Fin 2 → ℤ) (ha : ∀ (j : Fin 2), 0 ≤ a j ∧ a j ≤ ↑d) {L : ℝ} (hL : 0 ≤ L) (hcoeff : CoefficientHeightLE f ((↑d + 1) ^ (2 * (d + 1)) * L)) (m : Fin 2 →₀ ℕ) : |↑(((affineChart 2) ((homogeneousTranslation ℤ a) f)).coeff m)| ≤ leadingPositionHeightFactor d * L

Control the transformed coefficients through interpolation of translated grid values.

theorem CCDN.exists_translated_coefficient_position {d : ℕ} (hd : 0 < d) (f : MvPolynomial (Fin 3) ℤ) (hf : f.IsHomogeneous d) (hf0 : f ≠ 0) : ∃ (a : Fin 2 → ℤ) (H : ℝ), (∀ (j : Fin 2), 0 ≤ a j ∧ a j ≤ ↑d) ∧ 1 ≤ H ∧ CoefficientHeightLE ((affineChart 2) ((homogeneousTranslation ℤ a) f)) H ∧ Real.log |↑(MonomialOrder.lex.leadingCoeff ((homogeneousTranslation ℤ a) f))| ≤ Real.log H ∧ Real.log H ≤ Real.log |↑(MonomialOrder.lex.leadingCoeff ((homogeneousTranslation ℤ a) f))| + 14 * ↑d ^ 2

A bounded integer translation supplies the leading-position hypothesis with absolute constant 14, and a coefficient height at least one.