Roth's lemma

Roth's lemma bounds the index of a polynomial of small height at a point of large height. Let P ≠ 0 be a polynomial in n ≥ 1 variables over a number field K, with partial degrees deg_{Xᵢ} P ≤ rᵢ, where the weights rᵢ > 0 decrease quickly: rᵢ₊₁ ≤ σ rᵢ with 0 < σ ≤ 1 / 2. If every coordinate of β ∈ Kⁿ has relative logarithmic height rᵢ h(βᵢ) ≥ σ⁻¹ (h(P) + 4 n r₀ [K : ℚ]), then the weighted index of P at β satisfies

Ind_{β, r}(P) ≤ 2 n σ ^ (1 / 2 ^ (n - 1)).

In the proof of Roth's theorem this is the upper bound for the index of the auxiliary polynomial at a point of good rational approximations; it contradicts the large index of the auxiliary polynomial on the diagonal.

The proof is by induction on n. In one variable it is MvPolynomial.weightedIndex_toMvPolynomial_le. For n + 1 variables, separate the last variable, which has the smallest weight: P = ∑_{k < m} fₖ gₖ(Xₙ) with linearly independent families fₖ and gₖ (MvPolynomial.exists_sum_mul_linearIndependent). The determinant of the Hasse derivatives ∂^(μ k + l eₙ) P is the product of a nonzero generalized Wronskian W_μ(f) and the Hasse Wronskian of the gₖ, placed in Xₙ. Its height is bounded by MvPolynomial.logHeight_det_hasseDeriv_le, so the induction hypothesis bounds the index of W_μ(f) and the one-variable case bounds the index of the Hasse Wronskian. On the other hand, TauCeti.ofReal_mul_min_le_weightedIndex_genWronskian_add bounds the sum of these indices from below in terms of Ind_{β, r}(P); the two bounds are incompatible with a large index of P.

Main results

• TauCeti.weightedIndex_le_of_logHeight_le: Roth's lemma.

Implementation notes

The induction is carried out with the parameter θ = σ ^ (1 / 2 ^ (n - 1)), so that σ = θ ^ 2 ^ (n - 1). Passing from n + 1 to n variables replaces θ by θ ^ 2 and keeps σ, and no real powers occur inside the induction. If θ ≥ 1 / 2, the statement holds because the index is at most the number of variables; so the inductive step may assume θ < 1 / 2.

Heights are relative: h(P) is MvPolynomial.logHeight and h(βᵢ) is Height.logHeight₁.

References

• L. Pottmeyer, Diophantine Approximation (2022), §3.4, Theorem 3.4.1 and its proof.
• E. Bombieri and W. Gubler, Heights in Diophantine Geometry, Cambridge University Press (2006), Lemma 6.3.7.
• The induction in the parameter θ and the reduction to θ < 1 / 2 follow DiophantineApproximation/RothLemma.lean in Ralf Stephan's rwst/Subspace-Theorems, snapshot c26d909dc48cf7fe (Apache 2.0).

theorem TauCeti.weightedIndex_le_of_logHeight_le {K : Type u_1} [Field K] [NumberField K] {n : ℕ} [NeZero n] {P : MvPolynomial (Fin n) K} (hP : P ≠ 0) {r : Fin n → ℕ} (hr : ∀ (i : Fin n), 0 < r i) (hdeg : ∀ (i : Fin n), MvPolynomial.degreeOf i P ≤ r i) {σ : ℝ} (hσ₀ : 0 < σ) (hσ : σ ≤ 1 / 2) (hratio : ∀ (i j : Fin n), ↑j = ↑i + 1 → ↑(r j) ≤ σ * ↑(r i)) (β : Fin n → K) (hβ : ∀ (i : Fin n), σ⁻¹ * (P.logHeight + 4 * ↑n * ↑(r 0) * ↑(Module.finrank ℚ K)) ≤ ↑(r i) * Height.logHeight₁ (β i)) : MvPolynomial.weightedIndex r β P ≤ ENNReal.ofReal (2 * ↑n * σ ^ (1 / 2 ^ (n - 1)))

Roth's lemma (Pottmeyer, Theorem 3.4.1). Let P ≠ 0 be a polynomial in n ≥ 1 variables over a number field K, with partial degrees deg_{Xᵢ} P ≤ rᵢ for positive weights rᵢ satisfying rᵢ₊₁ ≤ σ rᵢ, where 0 < σ ≤ 1 / 2. If σ⁻¹ (h(P) + 4 n r₀ [K : ℚ]) ≤ rᵢ h(βᵢ) for every i, then the index of P at β with weights r is at most 2 n σ ^ (1 / 2 ^ (n - 1)). Heights are relative logarithmic heights.