Documentation

TauCeti.RingTheory.MvPolynomial.Abv.Coeff

Coefficient bounds for products and determinants of polynomials #

Let v be an absolute value on a commutative semiring R. If every coefficient of p and of q is bounded by r and s under v, then each coefficient of p * q is a sum of at most #p.support products of coefficients, so it is bounded by #p.support * (r * s). If v is nonarchimedean, the ultrametric inequality removes the count. Iterating gives bounds for finite products, and through the Leibniz expansion for determinants of matrices of polynomials: an m × m determinant has at most m! terms, each a product of m entries.

The product estimates allow semiring-valued absolute values. Finite products use a commutative domain as the value semiring so that v 1 = 1; the nonarchimedean estimates use a linear order, while the other product estimates need only a partial order.

A polynomial whose partial degrees are d j has at most ∏ j, (d j + 1) ≤ 2 ^ ∑ j, d j monomials, which turns the support counts into powers of two.

These are the local estimates behind height bounds for products of polynomials and for determinants of matrices of polynomials, such as the generalized Wronskians in the proof of Roth's lemma.

Main results #

References #

source
theorem MvPolynomial.card_support_le_prod_degreeOf {σ : Type u_1} {R : Type u_2} [Fintype σ] [CommSemiring R] (p : MvPolynomial σ R) :
p.support.card ≤ ∏ j : σ, (degreeOf j p + 1)

A polynomial in finitely many variables has at most ∏ j, (p.degreeOf j + 1) monomials.

source
theorem MvPolynomial.card_support_le_two_pow {σ : Type u_1} {R : Type u_2} [Fintype σ] [CommSemiring R] (p : MvPolynomial σ R) :
p.support.card ≤ 2 ^ ∑ j : σ, degreeOf j p

A polynomial in finitely many variables has at most 2 ^ ∑ j, p.degreeOf j monomials.

source
theorem MvPolynomial.abv_coeff_mul_le {σ : Type u_1} {R : Type u_2} {S : Type u_3} [CommSemiring R] [Semiring S] [PartialOrder S] [IsOrderedRing S] {v : AbsoluteValue R S} (p q : MvPolynomial σ R) {r s : S} (hp : ∀ (a : σ →₀ ℕ), v (p.coeff a) ≤ r) (hq : ∀ (a : σ →₀ ℕ), v (q.coeff a) ≤ s) (t : σ →₀ ℕ) :
v ((p * q).coeff t) ≤ ↑p.support.card * (r * s)

If the coefficients of p and q are bounded by r and s under an absolute value v, then each coefficient of p * q is bounded by #p.support * (r * s).

source
theorem MvPolynomial.abv_coeff_mul_le_of_isNonarchimedean {σ : Type u_1} {R : Type u_2} {S : Type u_3} [CommSemiring R] [Semiring S] [LinearOrder S] [PosMulMono S] [MulPosMono S] {v : AbsoluteValue R S} (p q : MvPolynomial σ R) (hv : IsNonarchimedean ⇑v) {r s : S} (hp : ∀ (a : σ →₀ ℕ), v (p.coeff a) ≤ r) (hq : ∀ (a : σ →₀ ℕ), v (q.coeff a) ≤ s) (t : σ →₀ ℕ) :
v ((p * q).coeff t) ≤ r * s

If v is nonarchimedean and the coefficients of p and q are bounded by r and s, then the coefficients of p * q are bounded by r * s.

source
theorem MvPolynomial.abv_coeff_prod_le {σ : Type u_1} {R : Type u_2} {S : Type u_3} [CommSemiring R] [Nontrivial R] [CommSemiring S] [PartialOrder S] [IsOrderedRing S] [IsDomain S] {v : AbsoluteValue R S} {ι : Type u_4} {s : Finset ι} (f : ι → MvPolynomial σ R) {C : ι → S} (hf : ∀ k ∈ s, ∀ (a : σ →₀ ℕ), v ((f k).coeff a) ≤ C k) (t : σ →₀ ℕ) :
v ((∏ k ∈ s, f k).coeff t) ≤ ∏ k ∈ s, ↑(f k).support.card * C k

If the coefficients of each f k are bounded by C k under an absolute value v, then each coefficient of ∏ k ∈ s, f k is bounded by ∏ k ∈ s, #(f k).support * C k.

source
theorem MvPolynomial.abv_coeff_prod_le_of_isNonarchimedean {σ : Type u_1} {R : Type u_2} {S : Type u_3} [CommSemiring R] [Nontrivial R] [CommSemiring S] [LinearOrder S] [IsOrderedRing S] [IsDomain S] {v : AbsoluteValue R S} {ι : Type u_4} {s : Finset ι} (f : ι → MvPolynomial σ R) (hv : IsNonarchimedean ⇑v) {C : ι → S} (hf : ∀ k ∈ s, ∀ (a : σ →₀ ℕ), v ((f k).coeff a) ≤ C k) (t : σ →₀ ℕ) :
v ((∏ k ∈ s, f k).coeff t) ≤ ∏ k ∈ s, C k

If v is nonarchimedean and the coefficients of each f k are bounded by C k, then the coefficients of ∏ k ∈ s, f k are bounded by ∏ k ∈ s, C k.

source
theorem MvPolynomial.abv_coeff_prod_le_two_pow {σ : Type u_1} {R : Type u_2} {S : Type u_3} [CommSemiring R] [Nontrivial R] [CommSemiring S] [PartialOrder S] [IsOrderedRing S] [IsDomain S] {v : AbsoluteValue R S} [Fintype σ] [NoZeroDivisors R] {ι : Type u_4} {s : Finset ι} (f : ι → MvPolynomial σ R) {C : ι → S} (hf : ∀ k ∈ s, ∀ (a : σ →₀ ℕ), v ((f k).coeff a) ≤ C k) (t : σ →₀ ℕ) :
v ((∏ k ∈ s, f k).coeff t) ≤ (2 ^ ∑ j : σ, degreeOf j (∏ k ∈ s, f k)) * ∏ k ∈ s, C k

If R has no zero divisors and the coefficients of each f k are bounded by C k under an absolute value v, then each coefficient of ∏ k ∈ s, f k is bounded by 2 ^ (∑ j, (∏ k ∈ s, f k).degreeOf j) * ∏ k ∈ s, C k.

source
theorem Matrix.abv_coeff_det_le {σ : Type u_1} {R : Type u_2} {S : Type u_3} [CommRing R] [Nontrivial R] [CommRing S] [LinearOrder S] [IsStrictOrderedRing S] {v : AbsoluteValue R S} {n : Type u_4} [Fintype n] [DecidableEq n] (A : Matrix n n (MvPolynomial σ R)) {B : ℕ} {C : S} (hB : ∀ (i j : n), (A i j).support.card ≤ B) (hA : ∀ (i j : n) (a : σ →₀ ℕ), v ((A i j).coeff a) ≤ C) (t : σ →₀ ℕ) :
v (A.det.coeff t) ≤ (Fintype.card n).factorial • (↑B * C) ^ Fintype.card n

If the entries of an n × n matrix of polynomials have at most B monomials each and coefficients bounded by C under an absolute value v, then each coefficient of its determinant is bounded by n! • (B * C) ^ n.

source
theorem Matrix.abv_coeff_det_le_of_isNonarchimedean {σ : Type u_1} {R : Type u_2} {S : Type u_3} [CommRing R] [Nontrivial R] [CommRing S] [LinearOrder S] [IsStrictOrderedRing S] {v : AbsoluteValue R S} {n : Type u_4} [Fintype n] [DecidableEq n] (A : Matrix n n (MvPolynomial σ R)) (hv : IsNonarchimedean ⇑v) {C : S} (hA : ∀ (i j : n) (a : σ →₀ ℕ), v ((A i j).coeff a) ≤ C) (t : σ →₀ ℕ) :
v (A.det.coeff t) ≤ C ^ Fintype.card n

If v is nonarchimedean and the entries of an n × n matrix of polynomials have coefficients bounded by C, then the coefficients of its determinant are bounded by C ^ n.