Coefficient heights under factorization

The product of the relative coefficient heights of nonzero polynomials over a number field is bounded by the coefficient height of their product, times a power of two. The exponent is the field degree times the degree of the product. The logarithmic form bounds the sum of factor heights and is useful for controlling roots with multiplicity.

The local height formula uses Gauss norms. At finite places they are multiplicative; at infinite places the complex Gelfond bound supplies the power of two. The height normalization is relative: divide logarithmic heights by the field degree to obtain the corresponding absolute estimate.

References

• Lukas Pottmeyer, Diophantine Approximation (17 January 2022), §3.2, Lemma 3.2.10 and Proposition 3.2.12.

theorem Polynomial.mulHeight_eq_of_numberField {K : Type u_1} [Field K] [NumberField K] {p : Polynomial K} (hp : p ≠ 0) : p.mulHeight = (∏ v : NumberField.InfinitePlace K, gaussNorm (↑v) 1 p ^ v.mult) * ∏ᶠ (v : NumberField.FinitePlace K), gaussNorm (↑v) 1 p

The relative coefficient height is the product of local Gauss norms, with the real or complex multiplicity at infinite places.

theorem Polynomial.hasFiniteMulSupport_gaussNorm {K : Type u_1} [Field K] [NumberField K] {p : Polynomial K} (hp : p ≠ 0) : Function.HasFiniteMulSupport fun (v : NumberField.FinitePlace K) => gaussNorm (↑v) 1 p

A nonzero polynomial has local coefficient norm one at all but finitely many finite places.

theorem Polynomial.prod_mulHeight_le_two_pow_mul_mulHeight_prod {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} (s : Finset ι) (f : ι → Polynomial K) (hf : ∀ i ∈ s, f i ≠ 0) : ∏ i ∈ s, (f i).mulHeight ≤ 2 ^ (Module.finrank ℚ K * (∏ i ∈ s, f i).natDegree) * (∏ i ∈ s, f i).mulHeight

The Gelfond bound for relative coefficient heights of a finite family of nonzero polynomials. The exponent depends on the degree of their product, not their number.

theorem Polynomial.sum_logHeight_le_logHeight_prod_add {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} (s : Finset ι) (f : ι → Polynomial K) (hf : ∀ i ∈ s, f i ≠ 0) : ∑ i ∈ s, (f i).logHeight ≤ (∏ i ∈ s, f i).logHeight + ↑(Module.finrank ℚ K) * ↑(∏ i ∈ s, f i).natDegree * Real.log 2

The logarithmic Gelfond bound for a finite family of nonzero polynomials over a number field, with relative coefficient heights.

theorem Polynomial.mulHeight_mulHeight_le_two_pow_mul_mulHeight {K : Type u_1} [Field K] [NumberField K] (f g : Polynomial K) (hf : f ≠ 0) (hg : g ≠ 0) : f.mulHeight * g.mulHeight ≤ 2 ^ (Module.finrank ℚ K * (f * g).natDegree) * (f * g).mulHeight

The product of the heights of two nonzero polynomial factors is controlled by the height of their product and its degree.

theorem Polynomial.logHeight_add_logHeight_le_logHeight_mul_add {K : Type u_1} [Field K] [NumberField K] (f g : Polynomial K) (hf : f ≠ 0) (hg : g ≠ 0) : f.logHeight + g.logHeight ≤ (f * g).logHeight + ↑(Module.finrank ℚ K) * ↑(f * g).natDegree * Real.log 2

The sum of the relative logarithmic heights of two nonzero polynomial factors is at most the height of their product plus the field degree times its degree times log 2.