Degrees of polynomials #
This file establishes many results about the degree of a multivariate polynomial.
The degree set of a polynomial $P \in R[X]$ is a Multiset containing, for each $x$ in the
variable set, $n$ copies of $x$, where $n$ is the maximum number of copies of $x$ appearing in a
monomial of $P$.
Main declarations #
-
MvPolynomial.degrees p: the multiset of variables representing the union of the multisets corresponding to each non-zero monomial inp. For example if7 ≠ 0inRandp = x²y+7y³thendegrees p = {x, x, y, y, y} -
MvPolynomial.degreeOf n p : ℕ: the total degree ofpwith respect to the variablen. For example ifp = x⁴y+yzthendegreeOf y p = 1. -
MvPolynomial.totalDegree p : ℕ: the max of the sizes of the multisetsswhose monomialsX^soccur inp. For example ifp = x⁴y+yzthentotalDegree p = 5.
Notation #
As in other polynomial files, we typically use the notation:
-
σ τ : Type*(indexing the variables) -
R : Type*[CommSemiring R](the coefficients) -
s : σ →₀ ℕ, a function fromσtoℕwhich is zero away from a finite set. This will give rise to a monomial inMvPolynomial σ Rwhich mathematicians might callX^s -
r : R -
i : σ, with corresponding monomialX i, often denotedX_iby mathematicians -
p : MvPolynomial σ R
def
MvPolynomial.degrees
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
(p : MvPolynomial σ R)
:
Multiset σ
The maximal degrees of each variable in a multi-variable polynomial, expressed as a multiset.
(For example, degrees (x^2 * y + y^3) would be {x, x, y, y, y}.)
Instances For
theorem
MvPolynomial.degrees_def
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
[DecidableEq σ]
(p : MvPolynomial σ R)
:
theorem
MvPolynomial.degrees_monomial
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
(s : σ →₀ ℕ)
(a : R)
:
((MvPolynomial.monomial s) a).degrees ≤ Finsupp.toMultiset s
theorem
MvPolynomial.degrees_monomial_eq
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
(s : σ →₀ ℕ)
(a : R)
(ha : a ≠ 0)
:
((MvPolynomial.monomial s) a).degrees = Finsupp.toMultiset s
theorem
MvPolynomial.degrees_C
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
(a : R)
:
(MvPolynomial.C a).degrees = 0
theorem
MvPolynomial.degrees_X'
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
(n : σ)
:
(MvPolynomial.X n).degrees ≤ {n}
@[simp]
theorem
MvPolynomial.degrees_X
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
[Nontrivial R]
(n : σ)
:
(MvPolynomial.X n).degrees = {n}
@[simp]
@[simp]
theorem
MvPolynomial.degrees_add
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
[DecidableEq σ]
(p : MvPolynomial σ R)
(q : MvPolynomial σ R)
:
theorem
MvPolynomial.degrees_sum
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
{ι : Type u_3}
[DecidableEq σ]
(s : Finset ι)
(f : ι → MvPolynomial σ R)
:
(s.sum fun (i : ι) => f i).degrees ≤ s.sup fun (i : ι) => (f i).degrees
theorem
MvPolynomial.degrees_mul
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
(p : MvPolynomial σ R)
(q : MvPolynomial σ R)
:
theorem
MvPolynomial.degrees_prod
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
{ι : Type u_3}
(s : Finset ι)
(f : ι → MvPolynomial σ R)
:
(s.prod fun (i : ι) => f i).degrees ≤ s.sum fun (i : ι) => (f i).degrees
theorem
MvPolynomial.degrees_pow
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
(p : MvPolynomial σ R)
(n : ℕ)
:
theorem
MvPolynomial.mem_degrees
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
{p : MvPolynomial σ R}
{i : σ}
:
theorem
MvPolynomial.le_degrees_add
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
{p : MvPolynomial σ R}
{q : MvPolynomial σ R}
(h : p.degrees.Disjoint q.degrees)
:
theorem
MvPolynomial.degrees_add_of_disjoint
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
[DecidableEq σ]
{p : MvPolynomial σ R}
{q : MvPolynomial σ R}
(h : p.degrees.Disjoint q.degrees)
:
theorem
MvPolynomial.degrees_map
{R : Type u}
{S : Type v}
{σ : Type u_1}
[CommSemiring R]
[CommSemiring S]
(p : MvPolynomial σ R)
(f : R →+* S)
:
((MvPolynomial.map f) p).degrees ⊆ p.degrees
theorem
MvPolynomial.degrees_rename
{R : Type u}
{σ : Type u_1}
{τ : Type u_2}
[CommSemiring R]
(f : σ → τ)
(φ : MvPolynomial σ R)
:
((MvPolynomial.rename f) φ).degrees ⊆ Multiset.map f φ.degrees
theorem
MvPolynomial.degrees_map_of_injective
{R : Type u}
{S : Type v}
{σ : Type u_1}
[CommSemiring R]
[CommSemiring S]
(p : MvPolynomial σ R)
{f : R →+* S}
(hf : Function.Injective ⇑f)
:
((MvPolynomial.map f) p).degrees = p.degrees
theorem
MvPolynomial.degrees_rename_of_injective
{R : Type u}
{σ : Type u_1}
{τ : Type u_2}
[CommSemiring R]
{p : MvPolynomial σ R}
{f : σ → τ}
(h : Function.Injective f)
:
((MvPolynomial.rename f) p).degrees = Multiset.map f p.degrees
def
MvPolynomial.degreeOf
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
(n : σ)
(p : MvPolynomial σ R)
:
degreeOf n p gives the highest power of X_n that appears in p
Equations
- MvPolynomial.degreeOf n p = Multiset.count n p.degrees
Instances For
theorem
MvPolynomial.degreeOf_def
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
[DecidableEq σ]
(n : σ)
(p : MvPolynomial σ R)
:
MvPolynomial.degreeOf n p = Multiset.count n p.degrees
theorem
MvPolynomial.degreeOf_eq_sup
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
(n : σ)
(f : MvPolynomial σ R)
:
MvPolynomial.degreeOf n f = f.support.sup fun (m : σ →₀ ℕ) => m n
theorem
MvPolynomial.degreeOf_lt_iff
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
{n : σ}
{f : MvPolynomial σ R}
{d : ℕ}
(h : 0 < d)
:
MvPolynomial.degreeOf n f < d ↔ ∀ m ∈ f.support, m n < d
theorem
MvPolynomial.degreeOf_le_iff
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
{n : σ}
{f : MvPolynomial σ R}
{d : ℕ}
:
MvPolynomial.degreeOf n f ≤ d ↔ ∀ m ∈ f.support, m n ≤ d
@[simp]
theorem
MvPolynomial.degreeOf_zero
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
(n : σ)
:
MvPolynomial.degreeOf n 0 = 0
@[simp]
theorem
MvPolynomial.degreeOf_C
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
(a : R)
(x : σ)
:
MvPolynomial.degreeOf x (MvPolynomial.C a) = 0
theorem
MvPolynomial.degreeOf_X
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
[DecidableEq σ]
(i : σ)
(j : σ)
[Nontrivial R]
:
MvPolynomial.degreeOf i (MvPolynomial.X j) = if i = j then 1 else 0
theorem
MvPolynomial.degreeOf_add_le
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
(n : σ)
(f : MvPolynomial σ R)
(g : MvPolynomial σ R)
:
MvPolynomial.degreeOf n (f + g) ≤ max (MvPolynomial.degreeOf n f) (MvPolynomial.degreeOf n g)
theorem
MvPolynomial.monomial_le_degreeOf
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
(i : σ)
{f : MvPolynomial σ R}
{m : σ →₀ ℕ}
(h_m : m ∈ f.support)
:
m i ≤ MvPolynomial.degreeOf i f
theorem
MvPolynomial.degreeOf_mul_le
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
(i : σ)
(f : MvPolynomial σ R)
(g : MvPolynomial σ R)
:
MvPolynomial.degreeOf i (f * g) ≤ MvPolynomial.degreeOf i f + MvPolynomial.degreeOf i g
theorem
MvPolynomial.degreeOf_mul_X_ne
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
{i : σ}
{j : σ}
(f : MvPolynomial σ R)
(h : i ≠ j)
:
MvPolynomial.degreeOf i (f * MvPolynomial.X j) = MvPolynomial.degreeOf i f
theorem
MvPolynomial.degreeOf_mul_X_eq
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
(j : σ)
(f : MvPolynomial σ R)
:
MvPolynomial.degreeOf j (f * MvPolynomial.X j) ≤ MvPolynomial.degreeOf j f + 1
theorem
MvPolynomial.degreeOf_C_mul_le
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
(p : MvPolynomial σ R)
(i : σ)
(c : R)
:
MvPolynomial.degreeOf i (MvPolynomial.C c * p) ≤ MvPolynomial.degreeOf i p
theorem
MvPolynomial.degreeOf_mul_C_le
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
(p : MvPolynomial σ R)
(i : σ)
(c : R)
:
MvPolynomial.degreeOf i (p * MvPolynomial.C c) ≤ MvPolynomial.degreeOf i p
theorem
MvPolynomial.degreeOf_rename_of_injective
{R : Type u}
{σ : Type u_1}
{τ : Type u_2}
[CommSemiring R]
{p : MvPolynomial σ R}
{f : σ → τ}
(h : Function.Injective f)
(i : σ)
:
MvPolynomial.degreeOf (f i) ((MvPolynomial.rename f) p) = MvPolynomial.degreeOf i p
totalDegree p gives the maximum |s| over the monomials X^s in p
Instances For
theorem
MvPolynomial.totalDegree_eq
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
(p : MvPolynomial σ R)
:
theorem
MvPolynomial.le_totalDegree
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
{p : MvPolynomial σ R}
{s : σ →₀ ℕ}
(h : s ∈ p.support)
:
theorem
MvPolynomial.totalDegree_le_degrees_card
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
(p : MvPolynomial σ R)
:
p.totalDegree ≤ Multiset.card p.degrees
theorem
MvPolynomial.totalDegree_le_of_support_subset
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
{p : MvPolynomial σ R}
{q : MvPolynomial σ R}
(h : p.support ⊆ q.support)
:
p.totalDegree ≤ q.totalDegree
@[simp]
theorem
MvPolynomial.totalDegree_C
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
(a : R)
:
(MvPolynomial.C a).totalDegree = 0
@[simp]
@[simp]
@[simp]
theorem
MvPolynomial.totalDegree_X
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
[Nontrivial R]
(s : σ)
:
(MvPolynomial.X s).totalDegree = 1
theorem
MvPolynomial.totalDegree_add
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
(a : MvPolynomial σ R)
(b : MvPolynomial σ R)
:
theorem
MvPolynomial.totalDegree_add_eq_left_of_totalDegree_lt
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
{p : MvPolynomial σ R}
{q : MvPolynomial σ R}
(h : q.totalDegree < p.totalDegree)
:
theorem
MvPolynomial.totalDegree_add_eq_right_of_totalDegree_lt
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
{p : MvPolynomial σ R}
{q : MvPolynomial σ R}
(h : q.totalDegree < p.totalDegree)
:
theorem
MvPolynomial.totalDegree_mul
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
(a : MvPolynomial σ R)
(b : MvPolynomial σ R)
:
theorem
MvPolynomial.totalDegree_smul_le
{R : Type u}
{S : Type v}
{σ : Type u_1}
[CommSemiring R]
[CommSemiring S]
[DistribMulAction R S]
(a : R)
(f : MvPolynomial σ S)
:
theorem
MvPolynomial.totalDegree_pow
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
(a : MvPolynomial σ R)
(n : ℕ)
:
@[simp]
theorem
MvPolynomial.totalDegree_monomial
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
(s : σ →₀ ℕ)
{c : R}
(hc : c ≠ 0)
:
((MvPolynomial.monomial s) c).totalDegree = s.sum fun (x : σ) (e : ℕ) => e
theorem
MvPolynomial.totalDegree_monomial_le
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
(s : σ →₀ ℕ)
(c : R)
:
((MvPolynomial.monomial s) c).totalDegree ≤ s.sum fun (x : σ) => id
@[simp]
theorem
MvPolynomial.totalDegree_X_pow
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
[Nontrivial R]
(s : σ)
(n : ℕ)
:
(MvPolynomial.X s ^ n).totalDegree = n
theorem
MvPolynomial.totalDegree_list_prod
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
(s : List (MvPolynomial σ R))
:
theorem
MvPolynomial.totalDegree_multiset_prod
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
(s : Multiset (MvPolynomial σ R))
:
s.prod.totalDegree ≤ (Multiset.map MvPolynomial.totalDegree s).sum
theorem
MvPolynomial.totalDegree_finset_prod
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
{ι : Type u_3}
(s : Finset ι)
(f : ι → MvPolynomial σ R)
:
(s.prod f).totalDegree ≤ s.sum fun (i : ι) => (f i).totalDegree
theorem
MvPolynomial.totalDegree_finset_sum
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
{ι : Type u_3}
(s : Finset ι)
(f : ι → MvPolynomial σ R)
:
(s.sum f).totalDegree ≤ s.sup fun (i : ι) => (f i).totalDegree
theorem
MvPolynomial.degreeOf_le_totalDegree
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
(f : MvPolynomial σ R)
(i : σ)
:
MvPolynomial.degreeOf i f ≤ f.totalDegree
theorem
MvPolynomial.exists_degree_lt
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
[Fintype σ]
(f : MvPolynomial σ R)
(n : ℕ)
(h : f.totalDegree < n * Fintype.card σ)
{d : σ →₀ ℕ}
(hd : d ∈ f.support)
:
∃ (i : σ), d i < n
theorem
MvPolynomial.coeff_eq_zero_of_totalDegree_lt
{R : Type u}
{σ : Type u_1}
[CommSemiring R]
{f : MvPolynomial σ R}
{d : σ →₀ ℕ}
(h : f.totalDegree < d.support.sum fun (i : σ) => d i)
:
MvPolynomial.coeff d f = 0
theorem
MvPolynomial.totalDegree_rename_le
{R : Type u}
{σ : Type u_1}
{τ : Type u_2}
[CommSemiring R]
(f : σ → τ)
(p : MvPolynomial σ R)
:
((MvPolynomial.rename f) p).totalDegree ≤ p.totalDegree