The maximum absolute coefficient height of an integer polynomial, and the hypothesis CoefficientHeightLE f H that it is at most a real bound H.

def CCDN.integerCoefficientHeight {σ : Type u_1} (f : MvPolynomial σ ℤ) : ℕ

The height of an integer polynomial: the maximum absolute value of its coefficients, or 0 for the zero polynomial.

Equations

• CCDN.integerCoefficientHeight f = f.support.sup fun (m : σ →₀ ℕ) => (f.coeff m).natAbs

@[reducible, inline]

abbrev CCDN.CoefficientHeightLE {σ : Type u_1} (f : MvPolynomial σ ℤ) (H : ℝ) : Prop

Every coefficient of f has absolute value at most the real bound H, that is, the coefficient height of f is at most H (coefficientHeightLE_iff).

Equations

• CCDN.CoefficientHeightLE f H = ∀ (m : σ →₀ ℕ), |↑(f.coeff m)| ≤ H

theorem CCDN.coefficient_abs_le_integerCoefficientHeight {σ : Type u_1} (f : MvPolynomial σ ℤ) (m : σ →₀ ℕ) : |↑(f.coeff m)| ≤ ↑(integerCoefficientHeight f)

Every coefficient of f has absolute value at most the coefficient height of f.

theorem CCDN.integerCoefficientHeight_le {σ : Type u_1} (f : MvPolynomial σ ℤ) {H : ℝ} (hH : 0 ≤ H) (hc : CoefficientHeightLE f H) : ↑(integerCoefficientHeight f) ≤ H

If every coefficient of f has absolute value at most a nonnegative real H, then the coefficient height of f is at most H.

theorem CCDN.coefficientHeightLE_iff {σ : Type u_1} {f : MvPolynomial σ ℤ} {H : ℝ} : CoefficientHeightLE f H ↔ ↑(integerCoefficientHeight f) ≤ H

A real bound on all coefficients is the same as a bound on the coefficient height.

theorem CCDN.integerCoefficientHeight_pos {σ : Type u_1} (f : MvPolynomial σ ℤ) (hf : f ≠ 0) : 0 < integerCoefficientHeight f

A nonzero integer polynomial has positive coefficient height.