Heights bound root multiplicities

A root β of multiplicity m of a polynomial P over a number field K contributes the factor (X - β) ^ m, whose m linear factors each have coefficient height H(β). Gelfond's inequality bounds the product of the heights of the factors by the height of P, which gives

m * h(β) ≤ h(P) + [K : ℚ] * deg P * log 2

for relative logarithmic heights. Thus a polynomial of small height cannot vanish to high order at a point of large height. In terms of indices: if P ≠ 0, r ≥ deg P and r * h(β) is at least s⁻¹ * (h(P) + [K : ℚ] * r * log 2) for some s > 0, then the index of P at β with weight r is at most s. This is Roth's lemma in one variable, the base case of the inductive bound on indices of auxiliary polynomials in the proof of Roth's theorem.

Main results

• Polynomial.rootMultiplicity_mul_logHeight₁_le: m * h(β) ≤ h(P) + [K : ℚ] * deg P * log 2.
• MvPolynomial.weightedIndex_toMvPolynomial_le: the index form of Roth's lemma in one variable, for a univariate polynomial placed in one coordinate.

References

• L. Pottmeyer, Diophantine Approximation (2022), §3.4, Lemma 3.4.3.
• The statement of the corresponding lemma in Ralf Stephan's DiophantineApproximation/RothBaseCase.lean in rwst/Subspace-Theorems, snapshot c26d909dc48cf7fe (Apache 2.0), was consulted for reference; the proof here is independent.

theorem Polynomial.rootMultiplicity_mul_logHeight₁_le {K : Type u_1} [Field K] [NumberField K] (P : Polynomial K) (β : K) : ↑(rootMultiplicity β P) * Height.logHeight₁ β ≤ P.logHeight + ↑(Module.finrank ℚ K) * ↑P.natDegree * Real.log 2

Roth's lemma in one variable, multiplicity form: the multiplicity of a root β of a polynomial P over a number field, times the relative logarithmic height of β, is at most h(P) + [K : ℚ] * deg P * log 2. The zero polynomial has root multiplicity zero.

theorem MvPolynomial.weightedIndex_toMvPolynomial_le {K : Type u_1} [Field K] [NumberField K] {σ : Type u_2} (r : σ → ℕ) (a : σ → K) (i : σ) {P : Polynomial K} (hP : P ≠ 0) (hr : P.natDegree ≤ r i) {s : ℝ} (hs : 0 < s) (h : s⁻¹ * (P.logHeight + ↑(Module.finrank ℚ K) * ↑(r i) * Real.log 2) ≤ ↑(r i) * Height.logHeight₁ (a i)) : weightedIndex r a ((Polynomial.toMvPolynomial i) P) ≤ ENNReal.ofReal s

Roth's lemma in one variable, index form. Let P ≠ 0 be placed in the coordinate i, with deg P ≤ r i. If r i * h(a i) ≥ s⁻¹ * (h(P) + [K : ℚ] * r i * log 2) for some s > 0, then the index of P at a with weights r is at most s. Heights are relative. Replacing log 2 by a larger constant, such as Pottmeyer's 4, only strengthens the hypothesis.