Naive height of an algebraic number

The naive height is the largest absolute value of a coefficient of the primitive integer minimal polynomial. It is defined in every characteristic-zero field, without a chosen complex embedding, and is constant on conjugacy classes. The value at a transcendental element is one.

For rational numbers it agrees with the multiplicative Weil height. For general algebraic numbers it instead measures the size of their defining polynomial; its bounds control denominators and the norms of real or complex roots, and norm_aeval_primitiveMinpoly_le bounds the primitive minimal polynomial near its complex roots.

References

• J.-H. Evertse, Diophantine Approximation (2019), ch. 3, §3.1, Exercise 3.1, and ch. 6, §6.1.

noncomputable def TauCeti.naiveHeight {F : Type u_1} [Field F] [CharZero F] (x : F) : ℝ

The coefficient sup norm of the primitive integer minimal polynomial. Its value at a transcendental element is one.

theorem TauCeti.naiveHeight_def {F : Type u_1} [Field F] [CharZero F] (x : F) : naiveHeight x = (primitiveMinpoly x).supNorm

Naive height is the native coefficient sup norm of the primitive minimal polynomial.

theorem TauCeti.naiveHeight_eq_iSup {F : Type u_1} [Field F] [CharZero F] (x : F) : naiveHeight x = ⨆ (i : ℕ), ‖(primitiveMinpoly x).coeff i‖

The naive height is the supremum of the absolute values of the coefficients.

theorem TauCeti.naiveHeight_eq_of_minpoly_eq {F : Type u_1} {F' : Type u_2} [Field F] [CharZero F] [Field F'] [CharZero F'] {x : F} {y : F'} (h : minpoly ℚ x = minpoly ℚ y) : naiveHeight x = naiveHeight y

Conjugates, even in different ambient fields, have equal naive height.

@[simp]

theorem TauCeti.naiveHeight_map {F : Type u_1} {F' : Type u_2} [Field F] [CharZero F] [Field F'] [CharZero F'] (f : F →+* F') (x : F) : naiveHeight (f x) = naiveHeight x

Field embeddings preserve naive height.

@[simp]

theorem TauCeti.naiveHeight_of_not_isAlgebraic {F : Type u_1} [Field F] [CharZero F] {x : F} (hx : ¬IsAlgebraic ℚ x) : naiveHeight x = 1

Transcendental elements have naive height one.

theorem TauCeti.norm_coeff_primitiveMinpoly_le_naiveHeight {F : Type u_1} [Field F] [CharZero F] (x : F) (i : ℕ) : ‖(primitiveMinpoly x).coeff i‖ ≤ naiveHeight x

The naive height bounds each coefficient of the primitive minimal polynomial.

theorem TauCeti.leadingCoeff_primitiveMinpoly_le_naiveHeight {F : Type u_1} [Field F] [CharZero F] (x : F) : ↑(primitiveMinpoly x).leadingCoeff ≤ naiveHeight x

The positive leading coefficient is bounded by the naive height.

theorem TauCeti.one_le_naiveHeight {F : Type u_1} [Field F] [CharZero F] (x : F) : 1 ≤ naiveHeight x

Naive height is at least one, including at transcendental elements.

theorem TauCeti.natDenominator_le_naiveHeight {F : Type u_1} [Field F] [CharZero F] (x : F) : ↑(Algebra.natDenominator x) ≤ naiveHeight x

The natural denominator is at most the naive height. For a transcendental element the natural denominator is the junk value 0.

@[simp]

theorem TauCeti.naiveHeight_ratCast {F : Type u_1} [Field F] [CharZero F] (q : ℚ) : naiveHeight ↑q = max ↑q.num.natAbs ↑q.den

The naive height of a rational number is the maximum of its numerator's absolute value and its positive denominator, independently of the ambient field.

theorem TauCeti.naiveHeight_ratCast_eq_mulHeight₁ {F : Type u_1} [Field F] [CharZero F] (q : ℚ) : naiveHeight ↑q = Height.mulHeight₁ q

On rational numbers naive height agrees with the multiplicative Weil height.

@[simp]

theorem TauCeti.naiveHeight_intCast {F : Type u_1} [Field F] [CharZero F] (n : ℤ) : naiveHeight ↑n = max |↑n| 1

The naive height of an integer is the maximum of its modulus and one.

@[simp]

theorem TauCeti.naiveHeight_zero {F : Type u_1} [Field F] [CharZero F] : naiveHeight 0 = 1

@[simp]

theorem TauCeti.naiveHeight_one {F : Type u_1} [Field F] [CharZero F] : naiveHeight 1 = 1

@[simp]

theorem TauCeti.naiveHeight_inv {F : Type u_1} [Field F] [CharZero F] (x : F) : naiveHeight x⁻¹ = naiveHeight x

Inversion preserves naive height, also at zero and at transcendental elements.

theorem TauCeti.norm_le_naiveHeight_add_one {K : Type u_3} [RCLike K] {x : K} (hx : IsAlgebraic ℚ x) : ‖x‖ ≤ naiveHeight x + 1

The norm of a real or complex algebraic number is bounded by its naive height plus one.

theorem TauCeti.inv_naiveHeight_add_one_le_norm {K : Type u_3} [RCLike K] {x : K} (hx : IsAlgebraic ℚ x) (hx0 : x ≠ 0) : (naiveHeight x + 1)⁻¹ ≤ ‖x‖

A nonzero real or complex algebraic number is bounded away from zero by its naive height.

theorem TauCeti.norm_aeval_primitiveMinpoly_le {α z : ℂ} (hα : IsAlgebraic ℚ α) : ‖(Polynomial.aeval z) (primitiveMinpoly α)‖ ≤ (↑(minpoly ℚ α).natDegree + 1) * (2 + ‖z‖) ^ (minpoly ℚ α).natDegree * naiveHeight α * ‖z - α‖

Near a complex algebraic number α of degree d, its primitive minimal polynomial F_α is small: |F_α(z)| ≤ (d + 1) (2 + |z|) ^ d H(α) |z - α|, where H(α) is the naive height of α. The bound is only informative when |z - α| ≤ 1, but holds for every z.