Weighted indices of multivariate polynomials

The index at a point with natural weights r is the infimum of ∑ j, d j / r j over nonzero Hasse jets. Thus an index lower bound specifies exactly which jets must vanish. For a nonzero polynomial over a commutative semiring the infimum is attained, and positive weights make it finite. Every finite index is rational, even when some weights vanish. The reciprocal weights distinguish this index from a weighted total degree.

Division takes place in ℝ≥0∞: a positive exponent in a coordinate of weight zero has infinite cost. The constant jet has cost zero, even when some weights vanish.

The index behaves like an order of vanishing. Over a semiring without zero divisors it is additive on products, because it is the least weight of a monomial of the Taylor shift (MvPolynomial.weightedIndex_eq_iInf_support), and least weights of monomials add on products (MvPolynomial.iInf_support_weight_mul). A Hasse derivative ∂^d lowers it by at most the weight of d, scaling all weights by c divides it by c, and renaming the variables injectively preserves it. A univariate polynomial placed in one coordinate has its root multiplicity divided by that coordinate's weight as index. These rules are the calculus of indices used for auxiliary polynomials in the proof of Roth's theorem.

Main results

• MvPolynomial.ofReal_le_weightedIndex_of_eval_hasseDeriv_eq_zero: for a polynomial with partial degrees at most r, the index is at least a real threshold t once the jets ∂^d P with d ≤ r and ∑ j, d j / r j < t vanish.
• MvPolynomial.le_sum_div_of_le_weightedIndex: a nonzero jet ∂^d P at a point where the index is at least t has d ≤ r and real weight t ≤ ∑ j, d j / r j.
• MvPolynomial.weightedIndex_mul: Ind(P Q) = Ind(P) + Ind(Q) without zero divisors.
• MvPolynomial.le_weightedIndex_det: the index of a determinant is at least the sum over the columns of lower bounds for the indices of their entries.
• MvPolynomial.weightedIndex_le_weightedIndex_hasseDeriv_add: Ind(P) ≤ Ind(∂^d P) + ∑ j, d j / r j.
• MvPolynomial.weightedIndex_smul_weight: the index for the weights c • r is the index for r divided by c.
• MvPolynomial.weightedIndex_rename: renaming along an injective map preserves the index.
• MvPolynomial.weightedIndex_toMvPolynomial: a univariate polynomial placed in the coordinate i has index rootMultiplicity / r i.
• MvPolynomial.exists_hasseDeriv_eval_ne_zero: if a polynomial P has finite index at b, some Hasse derivative Q = ∂^d P satisfies Q(b) ≠ 0 and Ind_a(P) - Ind_b(P) ≤ Ind_a(Q) at every other point a, and has the same partial degree bounds and coefficients at most 2 ^ ∑ᵢ rᵢ times as large.

References

• L. Pottmeyer, Diophantine Approximation (2022), §2.6, Definition 2.6.2, Example 2.6.3 and Exercise 2.19; §3.4, Lemma 3.4.3 and §§3.4.6–3.4.7; §3.5, Lemma 3.5.7.
• The determinant bound MvPolynomial.le_weightedIndex_det follows MvPolynomial.le_index_det in DiophantineApproximation/RothDeterminant.lean of Ralf Stephan's rwst/Subspace-Theorems, snapshot c26d909dc48cf7fe (Apache 2.0).

noncomputable def MvPolynomial.weightedIndex {σ : Type u_1} {R : Type u_2} [CommSemiring R] (r : σ → ℕ) (a : σ → R) (P : MvPolynomial σ R) : ENNReal

The weighted index is the least reciprocal-weighted order of a nonzero Hasse jet; the infimum of the empty set is ⊤.

theorem MvPolynomial.weightedIndex_def {σ : Type u_1} {R : Type u_2} [CommSemiring R] (r : σ → ℕ) (a : σ → R) (P : MvPolynomial σ R) : weightedIndex r a P = ⨅ (d : σ →₀ ℕ), ⨅ (_ : (eval a) ((hasseDeriv d) P) ≠ 0), ∑ j ∈ d.support, ↑(d j) / ↑(r j)

The defining infimum, expressed as a sum of ratios over the derivative's support.

theorem MvPolynomial.weightedIndex_le {σ : Type u_1} {R : Type u_2} [CommSemiring R] {r : σ → ℕ} {a : σ → R} {P : MvPolynomial σ R} {d : σ →₀ ℕ} (hd : (eval a) ((hasseDeriv d) P) ≠ 0) : weightedIndex r a P ≤ (Finsupp.weight fun (j : σ) => (↑(r j))⁻¹) d

A nonzero jet bounds the index from above by its weight.

theorem MvPolynomial.le_sum_div_of_le_weightedIndex {σ : Type u_1} {R : Type u_2} [CommSemiring R] [Fintype σ] {P : MvPolynomial σ R} {r : σ → ℕ} (hdeg : ∀ (i : σ), degreeOf i P ≤ r i) {a : σ → R} {t : ℝ} (ht : ENNReal.ofReal t ≤ weightedIndex r a P) {d : σ →₀ ℕ} (hd : (eval a) ((hasseDeriv d) P) ≠ 0) : (∀ (i : σ), d i ≤ r i) ∧ t ≤ ∑ i : σ, ↑(d i) / ↑(r i)

A nonzero jet of a polynomial with partial degrees degreeOf i P ≤ r i and index at least t satisfies d ≤ r and has weight t ≤ ∑ᵢ dᵢ / rᵢ, computed in ℝ.

theorem MvPolynomial.le_weightedIndex_iff {σ : Type u_1} {R : Type u_2} [CommSemiring R] (r : σ → ℕ) (a : σ → R) (P : MvPolynomial σ R) (t : ENNReal) : t ≤ weightedIndex r a P ↔ ∀ (d : σ →₀ ℕ), ∑ j ∈ d.support, ↑(d j) / ↑(r j) < t → (eval a) ((hasseDeriv d) P) = 0

An index lower bound is equivalent to the vanishing of all jets of strictly smaller weight. The strict inequality also covers the threshold ⊤.

theorem MvPolynomial.ofReal_le_weightedIndex_of_eval_hasseDeriv_eq_zero {σ : Type u_1} {R : Type u_2} [CommSemiring R] [Fintype σ] {P : MvPolynomial σ R} {r : σ → ℕ} (hdeg : ∀ (i : σ), degreeOf i P ≤ r i) {a : σ → R} {t : ℝ} (h : ∀ (d : σ →₀ ℕ), (∀ (i : σ), d i ≤ r i) → ∑ i : σ, ↑(d i) / ↑(r i) < t → (eval a) ((hasseDeriv d) P) = 0) : ENNReal.ofReal t ≤ weightedIndex r a P

For a polynomial with partial degrees degreeOf i P ≤ r i, the index is at least a real threshold t as soon as the jets ∂^d P (a) vanish for every d ≤ r of real weight ∑ᵢ dᵢ / rᵢ < t.

@[simp]

theorem MvPolynomial.weightedIndex_zero {σ : Type u_1} {R : Type u_2} [CommSemiring R] (r : σ → ℕ) (a : σ → R) : weightedIndex r a 0 = ⊤

theorem MvPolynomial.min_weightedIndex_le_add {σ : Type u_1} {R : Type u_2} [CommSemiring R] (r : σ → ℕ) (a : σ → R) (P Q : MvPolynomial σ R) : min (weightedIndex r a P) (weightedIndex r a Q) ≤ weightedIndex r a (P + Q)

The index of a sum is at least the smaller index.

theorem MvPolynomial.le_weightedIndex_sum {σ : Type u_1} {R : Type u_2} [CommSemiring R] {ι : Type u_3} (r : σ → ℕ) (a : σ → R) {s : Finset ι} {P : ι → MvPolynomial σ R} {t : ENNReal} (h : ∀ i ∈ s, t ≤ weightedIndex r a (P i)) : t ≤ weightedIndex r a (∑ i ∈ s, P i)

The index of a finite sum is at least every common lower bound for the indices of the summands.

theorem MvPolynomial.weightedIndex_map {σ : Type u_1} {R : Type u_2} [CommSemiring R] {S : Type u_3} [CommSemiring S] (f : R →+* S) (hf : Function.Injective ⇑f) (r : σ → ℕ) (a : σ → R) (P : MvPolynomial σ R) : weightedIndex r (fun (j : σ) => f (a j)) ((map f) P) = weightedIndex r a P

Injective coefficient maps preserve the index when the center is mapped as well.

theorem MvPolynomial.weightedIndex_taylor {σ : Type u_1} {R : Type u_2} [CommSemiring R] (r : σ → ℕ) (a b : σ → R) (P : MvPolynomial σ R) : weightedIndex r b ((taylor a) P) = weightedIndex r (b + a) P

Taylor translation of the polynomial translates the center of its index.

theorem MvPolynomial.exists_weightedIndex_eq_weight {σ : Type u_1} {R : Type u_2} [CommSemiring R] {r : σ → ℕ} {a : σ → R} {P : MvPolynomial σ R} (hP : (taylor a) P ≠ 0) : ∃ (d : σ →₀ ℕ), (eval a) ((hasseDeriv d) P) ≠ 0 ∧ weightedIndex r a P = (Finsupp.weight fun (j : σ) => (↑(r j))⁻¹) d

The index is attained by a nonzero Taylor coefficient whenever the Taylor shift is nonzero. This statement also permits zero weights and infinite index.

theorem MvPolynomial.weightedIndex_eq_iInf_support {σ : Type u_1} {R : Type u_2} [CommSemiring R] (r : σ → ℕ) (a : σ → R) (P : MvPolynomial σ R) : weightedIndex r a P = ⨅ d ∈ ((taylor a) P).support, (Finsupp.weight fun (j : σ) => (↑(r j))⁻¹) d

The index is the least reciprocal weight of a monomial of the Taylor shift.

theorem MvPolynomial.weightedIndex_eq_top_of_taylor_eq_zero {σ : Type u_1} {R : Type u_2} [CommSemiring R] (r : σ → ℕ) {a : σ → R} {P : MvPolynomial σ R} (hP : (taylor a) P = 0) : weightedIndex r a P = ⊤

A polynomial whose Taylor shift vanishes has infinite index.

theorem MvPolynomial.weightedIndex_ne_top {σ : Type u_1} {R : Type u_2} [CommSemiring R] {r : σ → ℕ} (hr : ∀ (j : σ), r j ≠ 0) (a : σ → R) {P : MvPolynomial σ R} (hP : P ≠ 0) : weightedIndex r a P ≠ ⊤

Positive weights make the index of every nonzero polynomial finite.

@[simp]

theorem MvPolynomial.weightedIndex_eq_top_iff {σ : Type u_1} {R : Type u_2} [CommSemiring R] {r : σ → ℕ} (hr : ∀ (j : σ), r j ≠ 0) (a : σ → R) (P : MvPolynomial σ R) : weightedIndex r a P = ⊤ ↔ P = 0

With positive weights, infinite index characterizes the zero polynomial.

theorem MvPolynomial.weightedIndex_le_sum_degreeOf {σ : Type u_1} {R : Type u_2} [CommSemiring R] [Fintype σ] (r : σ → ℕ) (a : σ → R) {P : MvPolynomial σ R} (hP : P ≠ 0) : weightedIndex r a P ≤ ∑ j : σ, ↑(degreeOf j P) / ↑(r j)

A nonzero polynomial's index is bounded by the sum of its partial degrees divided by the corresponding weights.

theorem MvPolynomial.exists_weightedIndex_eq_nnrat {σ : Type u_1} {R : Type u_2} [CommSemiring R] {r : σ → ℕ} {a : σ → R} {P : MvPolynomial σ R} (hP : weightedIndex r a P ≠ ⊤) : ∃ (q : ℚ≥0), weightedIndex r a P = ↑↑q

Every finite index is a nonnegative rational number, even when some weights vanish.

@[simp]

theorem MvPolynomial.weightedIndex_eq_zero_iff {σ : Type u_1} {R : Type u_2} [CommSemiring R] (r : σ → ℕ) (a : σ → R) (P : MvPolynomial σ R) : weightedIndex r a P = 0 ↔ (eval a) P ≠ 0

Index zero detects nonvanishing at the center, without a positivity condition on the weights.

@[simp]

theorem MvPolynomial.weightedIndex_one {σ : Type u_1} {R : Type u_2} [CommSemiring R] [Nontrivial R] (r : σ → ℕ) (a : σ → R) : weightedIndex r a 1 = 0

theorem MvPolynomial.weightedIndex_monomial_zero {σ : Type u_1} {R : Type u_2} [CommSemiring R] (r : σ → ℕ) (d : σ →₀ ℕ) {c : R} (hc : c ≠ 0) : weightedIndex r 0 ((monomial d) c) = (Finsupp.weight fun (j : σ) => (↑(r j))⁻¹) d

At the origin a monomial has exactly the reciprocal-weighted degree of its exponent.

theorem MvPolynomial.le_weightedIndex_mul {σ : Type u_1} {R : Type u_2} [CommSemiring R] (r : σ → ℕ) (a : σ → R) (P Q : MvPolynomial σ R) : weightedIndex r a P + weightedIndex r a Q ≤ weightedIndex r a (P * Q)

The index of a product is at least the sum of the indices of the factors.

theorem MvPolynomial.le_weightedIndex_prod {σ : Type u_1} {R : Type u_2} [CommSemiring R] {ι : Type u_3} (r : σ → ℕ) (a : σ → R) (P : ι → MvPolynomial σ R) (s : Finset ι) : ∑ i ∈ s, weightedIndex r a (P i) ≤ weightedIndex r a (∏ i ∈ s, P i)

The index of a finite product is at least the sum of the indices of its factors.

theorem MvPolynomial.weightedIndex_le_weightedIndex_hasseDeriv_add {σ : Type u_1} {R : Type u_2} [CommSemiring R] (r : σ → ℕ) (a : σ → R) (d : σ →₀ ℕ) (P : MvPolynomial σ R) : weightedIndex r a P ≤ weightedIndex r a ((hasseDeriv d) P) + (Finsupp.weight fun (j : σ) => (↑(r j))⁻¹) d

A Hasse derivative ∂^d lowers the index by at most the weight of d: Ind(P) ≤ Ind(∂^d P) + ∑ j, d j / r j.

theorem MvPolynomial.weightedIndex_smul_weight {σ : Type u_1} {R : Type u_2} [CommSemiring R] (c : ℕ) (r : σ → ℕ) (a : σ → R) (P : MvPolynomial σ R) : weightedIndex (c • r) a P = weightedIndex r a P / ↑c

Multiplying every weight by a natural number c divides the index by c. This also holds for c = 0, using division in ℝ≥0∞.

theorem MvPolynomial.weightedIndex_rename {σ : Type u_1} {R : Type u_2} [CommSemiring R] {τ : Type u_3} {f : σ → τ} (hf : Function.Injective f) (r : τ → ℕ) (b : τ → R) (P : MvPolynomial σ R) : weightedIndex r b ((rename f) P) = weightedIndex (r ∘ f) (b ∘ f) P

Renaming the variables along an injective map preserves the index, when the center and the weights are pulled back along the map.

theorem MvPolynomial.weightedIndex_mul {σ : Type u_1} {R : Type u_2} [CommSemiring R] [NoZeroDivisors R] (r : σ → ℕ) (a : σ → R) (P Q : MvPolynomial σ R) : weightedIndex r a (P * Q) = weightedIndex r a P + weightedIndex r a Q

Over a semiring without zero divisors, the index of a product is the sum of the indices. This holds for all weights, including zero weights and infinite indices.

theorem MvPolynomial.weightedIndex_pow {σ : Type u_1} {R : Type u_2} [CommSemiring R] [NoZeroDivisors R] [Nontrivial R] (r : σ → ℕ) (a : σ → R) (P : MvPolynomial σ R) (n : ℕ) : weightedIndex r a (P ^ n) = n • weightedIndex r a P

Over a nontrivial semiring without zero divisors, the index of P ^ n is n times the index of P.

theorem MvPolynomial.weightedIndex_prod {σ : Type u_1} {R : Type u_2} [CommSemiring R] [NoZeroDivisors R] [Nontrivial R] {ι : Type u_3} (r : σ → ℕ) (a : σ → R) (P : ι → MvPolynomial σ R) (s : Finset ι) : weightedIndex r a (∏ i ∈ s, P i) = ∑ i ∈ s, weightedIndex r a (P i)

Over a nontrivial semiring without zero divisors, the index of a finite product is the sum of the indices of its factors.

@[simp]

theorem MvPolynomial.weightedIndex_neg {σ : Type u_1} {R : Type u_2} [CommRing R] (r : σ → ℕ) (a : σ → R) (P : MvPolynomial σ R) : weightedIndex r a (-P) = weightedIndex r a P

theorem MvPolynomial.le_weightedIndex_det {σ : Type u_1} {R : Type u_2} [CommRing R] {n : Type u_3} [Fintype n] [DecidableEq n] (r : σ → ℕ) (a : σ → R) (A : Matrix n n (MvPolynomial σ R)) {c : n → ENNReal} (h : ∀ (k l : n), c l ≤ weightedIndex r a (A k l)) : ∑ l : n, c l ≤ weightedIndex r a A.det

The index of a determinant is at least the sum over the columns of lower bounds for the indices of the entries of each column.

theorem MvPolynomial.weightedIndex_toMvPolynomial {σ : Type u_1} {R : Type u_2} [CommRing R] (r : σ → ℕ) (a : σ → R) (i : σ) {p : Polynomial R} (hp : p ≠ 0) : weightedIndex r a ((Polynomial.toMvPolynomial i) p) = ↑(Polynomial.rootMultiplicity (a i) p) / ↑(r i)

A nonzero univariate polynomial placed in the coordinate i has as index its root multiplicity at a i divided by the weight of i. This includes zero weights.

theorem MvPolynomial.weightedIndex_X_sub_C_pow {σ : Type u_1} {R : Type u_2} [CommRing R] [Nontrivial R] (r : σ → ℕ) (a : σ → R) (i : σ) (m : ℕ) : weightedIndex r a ((X i - C (a i)) ^ m) = ↑m / ↑(r i)

A power of a centered coordinate has its exponent divided by the coordinate's weight as index. This includes exponent zero and zero weights.

theorem MvPolynomial.exists_hasseDeriv_eval_ne_zero {σ : Type u_1} {R : Type u_2} {F : Type u_3} {K : Type u_4} {S : Type u_5} [Fintype σ] [CommSemiring R] [CommSemiring F] [CommSemiring K] [Semiring S] [PartialOrder S] [IsOrderedRing S] {P : MvPolynomial σ R} {r : σ → ℕ} (hdeg : ∀ (i : σ), degreeOf i P ≤ r i) (abv : AbsoluteValue R S) {B : S} (hB : ∀ (μ : σ →₀ ℕ), abv (P.coeff μ) ≤ B) (f : R →+* F) (a : σ → F) (g : R →+* K) {b : σ → K} (hb : weightedIndex r b ((map g) P) ≠ ⊤) : ∃ (d : σ →₀ ℕ), (eval b) ((map g) ((hasseDeriv d) P)) ≠ 0 ∧ weightedIndex r a ((map f) P) - weightedIndex r b ((map g) P) ≤ weightedIndex r a ((map f) ((hasseDeriv d) P)) ∧ (∀ (i : σ), degreeOf i ((hasseDeriv d) P) ≤ r i) ∧ ∀ (μ : σ →₀ ℕ), abv (((hasseDeriv d) P).coeff μ) ≤ (2 ^ ∑ i : σ, r i) * B

Choice of a nonvanishing Hasse derivative (the proof of Pottmeyer, Lemma 3.5.7). Let P be a polynomial with partial degrees degreeOf i P ≤ r i and coefficients of absolute value at most B. If the index of the image of P under g at a point b is finite, then some Hasse derivative Q = ∂^d P does not vanish at b after applying g, loses at most the index at b from its index at every point a after applying f, still has partial degrees at most r i, and has coefficients of absolute value at most 2 ^ ∑ᵢ rᵢ * B.