The index of the determinant in the inductive step of Roth's lemma

Roth's lemma bounds the weighted index Ind_{a, r}(P) of a polynomial P at a point a of large height. Its inductive step replaces P by the determinant

W = det (∂^(D k + l eᵢ) P)_{k, l < m}

of Hasse derivatives of P, where m ≤ r i + 1, and the rows D k have weight ∑ⱼ (D k)ⱼ / rⱼ ≤ c. If P = ∑ₖ fₖ · gₖ(Xᵢ) is separated in the variable Xᵢ and the rows do not differentiate in Xᵢ, then W is the product of the generalized Wronskian W_D(f) and the Hasse Wronskian of the gₖ placed in Xᵢ (MvPolynomial.det_hasseDeriv_sum_mul_toMvPolynomial). The heights and degrees of the two factors are controlled, so the induction hypothesis and the one-variable case bound their indices from above.

This file proves the matching lower bound. The entries of column l have index at least Ind(P) - c - l / r i, so the index of W is at least the sum of the positive parts of these numbers over l < m. By Pottmeyer's Lemma 3.4.8 (TauCeti.mul_min_le_sum_max_sub_div) this sum is at least m min (δ / 2) (δ² / 2) with δ = Ind(P) - c. A large index of P therefore forces a large index of one of the two Wronskians.

Main results

• TauCeti.ofReal_mul_min_le_weightedIndex_det_hasseDeriv: the lower bound m min (δ / 2) (δ² / 2) ≤ Ind(W), over any commutative ring.
• TauCeti.ofReal_mul_min_le_weightedIndex_genWronskian_add: for a separated polynomial over a ring without zero divisors, the same lower bound for the sum of the indices of the two Wronskians.

References

• L. Pottmeyer, Diophantine Approximation (2022), §3.4, proof of Theorem 3.4.1, §3.4.7 and Lemma 3.4.8.
• E. Bombieri and W. Gubler, Heights in Diophantine Geometry, Cambridge University Press (2006), proof of Lemma 6.3.7.
• The column-wise estimate follows the inductive step MvPolynomial.rothProp_succ in DiophantineApproximation/RothLemma.lean of Ralf Stephan's rwst/Subspace-Theorems, snapshot c26d909dc48cf7fe (Apache 2.0).

theorem TauCeti.ofReal_mul_min_le_weightedIndex_det_hasseDeriv {σ : Type u_1} {R : Type u_2} [CommRing R] {m : ℕ} {r : σ → ℕ} {a : σ → R} {P : MvPolynomial σ R} {i : σ} (hm : m ≤ r i + 1) (D : Fin m → σ →₀ ℕ) {t c : ℝ} (hc : 0 ≤ c) (ht : ENNReal.ofReal t ≤ MvPolynomial.weightedIndex r a P) (hD : ∀ (k : Fin m), (Finsupp.weight fun (j : σ) => (↑(r j))⁻¹) (D k) ≤ ENNReal.ofReal c) : ENNReal.ofReal (↑m * min ((t - c) / 2) ((t - c) ^ 2 / 2)) ≤ MvPolynomial.weightedIndex r a (Matrix.of fun (k l : Fin m) => (MvPolynomial.hasseDeriv (D k + Finsupp.single i ↑l)) P).det

The index of the determinant in Roth's lemma. Let P have index at least t at a with respect to the weights r, let m ≤ r i + 1, and let the rows D k have weight ∑ⱼ (D k)ⱼ / rⱼ ≤ c with c ≥ 0. Then the determinant of the Hasse derivatives ∂^(D k + l eᵢ) P, for k, l < m, has index at least m min (δ / 2) (δ² / 2), where δ = t - c.

theorem TauCeti.ofReal_mul_min_le_weightedIndex_genWronskian_add {σ : Type u_1} {R : Type u_2} [CommRing R] {m : ℕ} [NoZeroDivisors R] {r : σ → ℕ} {a : σ → R} {i : σ} (hm : m ≤ r i + 1) {D : Fin m → σ →₀ ℕ} (hDi : ∀ (k : Fin m), (D k) i = 0) {f : Fin m → MvPolynomial σ R} (hf : ∀ (k : Fin m), i ∉ (f k).vars) (g : Fin m → Polynomial R) {t c : ℝ} (hc : 0 ≤ c) (ht : ENNReal.ofReal t ≤ MvPolynomial.weightedIndex r a (∑ k : Fin m, f k * (Polynomial.toMvPolynomial i) (g k))) (hD : ∀ (k : Fin m), (Finsupp.weight fun (j : σ) => (↑(r j))⁻¹) (D k) ≤ ENNReal.ofReal c) : ENNReal.ofReal (↑m * min ((t - c) / 2) ((t - c) ^ 2 / 2)) ≤ MvPolynomial.weightedIndex r a (MvPolynomial.genWronskian D f) + MvPolynomial.weightedIndex r a ((Polynomial.toMvPolynomial i) (Polynomial.hasseWronskian g))

The index of the two Wronskians in Roth's lemma. Let P = ∑ₖ fₖ · gₖ(Xᵢ) over a ring without zero divisors, where no fₖ involves Xᵢ, and let the rows D k not differentiate in Xᵢ. Under the hypotheses of ofReal_mul_min_le_weightedIndex_det_hasseDeriv, the indices of the generalized Wronskian W_D(f) and of the Hasse Wronskian of the gₖ placed in Xᵢ add up to at least m min (δ / 2) (δ² / 2), where δ = t - c.