Choosing a Hasse derivative of Roth's auxiliary polynomial

In the proof of Roth's theorem, an integer auxiliary polynomial P vanishes to a high index at the diagonal point (α, …, α), while Roth's index estimate shows that its index at a tuple β of good rational approximations of α is small. The final step needs a polynomial that does not vanish at β at all. It is obtained as a Hasse derivative Q = ∂^d P, where d is a jet of P at β of minimal weight. Since ∂^d lowers indices by at most the weight of d, the index of Q at the diagonal point is still large, and the coefficients of Q are at most 2 ^ ∑ᵢ rᵢ times those of P, where the rᵢ bound the partial degrees of P.

The value Q(β) is then a nonzero rational number which is bounded from above using the large index of Q at the diagonal point, and from below by the denominators of β. Comparing the two bounds yields the contradiction which proves Roth's theorem.

Main results

• TauCeti.exists_roth_hasseDeriv: the choice of Q made by MvPolynomial.exists_hasseDeriv_eval_ne_zero, with the parameters of the proof of Roth's theorem. An index at least (n / 2) (1 - ε) at a and an index at most 5 n ε / 2 at b leave the derivative an index at least (1 / 2 - 3 ε) n at a, and coefficients at most exp (C₁ ∑ᵢ rᵢ) with ∑ᵢ rᵢ ≤ 2 D / L become coefficients at most exp (4 C₁ D / L).

References

• L. Pottmeyer, Diophantine Approximation (2022), §3.5, Lemma 3.5.7.

theorem TauCeti.exists_roth_hasseDeriv {σ : Type u_1} {F : Type u_2} {K : Type u_3} [Fintype σ] [CommRing F] [CommRing K] {P : MvPolynomial σ ℤ} {r : σ → ℕ} (hdeg : ∀ (i : σ), MvPolynomial.degreeOf i P ≤ r i) {ε C₁ D L : ℝ} (hε : 0 ≤ ε) (hC₁ : Real.log 2 ≤ C₁) (hr : ∑ i : σ, ↑(r i) ≤ 2 * D / L) (hP : ∀ (μ : σ →₀ ℕ), |↑(P.coeff μ)| ≤ Real.exp (C₁ * ∑ i : σ, ↑(r i))) {a : σ → F} {b : σ → K} (ha : ENNReal.ofReal (↑(Fintype.card σ) / 2 * (1 - ε)) ≤ MvPolynomial.weightedIndex r a ((MvPolynomial.map (Int.castRingHom F)) P)) (hb : MvPolynomial.weightedIndex r b ((MvPolynomial.map (Int.castRingHom K)) P) ≤ ENNReal.ofReal (5 * ↑(Fintype.card σ) * ε / 2)) : ∃ (d : σ →₀ ℕ), (MvPolynomial.eval b) ((MvPolynomial.map (Int.castRingHom K)) ((MvPolynomial.hasseDeriv d) P)) ≠ 0 ∧ ENNReal.ofReal ((1 / 2 - 3 * ε) * ↑(Fintype.card σ)) ≤ MvPolynomial.weightedIndex r a ((MvPolynomial.map (Int.castRingHom F)) ((MvPolynomial.hasseDeriv d) P)) ∧ (∀ (i : σ), MvPolynomial.degreeOf i ((MvPolynomial.hasseDeriv d) P) ≤ r i) ∧ ∀ (μ : σ →₀ ℕ), |↑(((MvPolynomial.hasseDeriv d) P).coeff μ)| ≤ Real.exp (4 * C₁ * D / L)

Pottmeyer, Lemma 3.5.7. The choice of a nonvanishing Hasse derivative of Roth's auxiliary polynomial. Let P be an integer polynomial in n variables with partial degrees degreeOf i P ≤ r i, where ∑ᵢ rᵢ ≤ 2 D / L, and with coefficients of absolute value at most exp (C₁ ∑ᵢ rᵢ), where C₁ ≥ log 2. Let 0 ≤ ε. If the index of P is at least (n / 2) (1 - ε) at a and at most 5 n ε / 2 at b, then some Hasse derivative Q = ∂^d P does not vanish at b, has index at least (1 / 2 - 3 ε) n at a, has partial degrees at most r i, and has coefficients of absolute value at most exp (4 C₁ D / L).