# 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 in `p`. For example if `7 ≠ 0` in `R` and `p = x²y+7y³` then `degrees p = {x, x, y, y, y}`

- `MvPolynomial.degreeOf n p : ℕ` : the total degree of `p` with respect to the variable `n`. For example if `p = x⁴y+yz` then `degreeOf y p = 1`.

- `MvPolynomial.totalDegree p : ℕ` : the max of the sizes of the multisets `s` whose monomials `X^s` occur in `p`. For example if `p = x⁴y+yz` then `totalDegree 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 in `MvPolynomial σ R` which mathematicians might call `X^s`

- `r : R`

- `i : σ`, with corresponding monomial `X i`, often denoted `X_i` by mathematicians

- `p : MvPolynomial σ R`

### `degrees` #

source
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}`.)

Equations

- p.degrees = p.support.sup fun (s : σ →₀ ℕ) => Finsupp.toMultiset s

Instances For

source
theorem MvPolynomial.degrees_def {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (p : MvPolynomial σ R) :
p.degrees = p.support.sup fun (s : σ →₀ ℕ) => Finsupp.toMultiset s
source
theorem MvPolynomial.degrees_monomial {R : Type u} {σ : Type u_1} [CommSemiring R] (s : σ →₀ ℕ) (a : R) :
((monomial s) a).degrees ≤ Finsupp.toMultiset s
source
theorem MvPolynomial.degrees_monomial_eq {R : Type u} {σ : Type u_1} [CommSemiring R] (s : σ →₀ ℕ) (a : R) (ha : a ≠ 0) :
((monomial s) a).degrees = Finsupp.toMultiset s
source
theorem MvPolynomial.degrees_C {R : Type u} {σ : Type u_1} [CommSemiring R] (a : R) :
(C a).degrees = 0
source
theorem MvPolynomial.degrees_X' {R : Type u} {σ : Type u_1} [CommSemiring R] (n : σ) :
(X n).degrees ≤ {n}
source
@[simp]
theorem MvPolynomial.degrees_X {R : Type u} {σ : Type u_1} [CommSemiring R] [Nontrivial R] (n : σ) :
(X n).degrees = {n}
source
@[simp]
theorem MvPolynomial.degrees_zero {R : Type u} {σ : Type u_1} [CommSemiring R] :
degrees 0 = 0
source
@[simp]
theorem MvPolynomial.degrees_one {R : Type u} {σ : Type u_1} [CommSemiring R] :
degrees 1 = 0
source
theorem MvPolynomial.degrees_add_le {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] {p q : MvPolynomial σ R} :
(p + q).degrees ≤ p.degrees ⊔ q.degrees
source
theorem MvPolynomial.degrees_sum_le {R : Type u} {σ : Type u_1} [CommSemiring R] {ι : Type u_3} [DecidableEq σ] (s : Finset ι) (f : ι → MvPolynomial σ R) :
(∑ i ∈ s, f i).degrees ≤ s.sup fun (i : ι) => (f i).degrees
source
theorem MvPolynomial.degrees_mul_le {R : Type u} {σ : Type u_1} [CommSemiring R] {p q : MvPolynomial σ R} :
(p * q).degrees ≤ p.degrees + q.degrees
source
theorem MvPolynomial.degrees_prod_le {R : Type u} {σ : Type u_1} [CommSemiring R] {ι : Type u_3} {s : Finset ι} {f : ι → MvPolynomial σ R} :
(∏ i ∈ s, f i).degrees ≤ ∑ i ∈ s, (f i).degrees
source
theorem MvPolynomial.degrees_pow_le {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} {n : ℕ} :
(p ^ n).degrees ≤ n • p.degrees
source
theorem MvPolynomial.mem_degrees {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} {i : σ} :
i ∈ p.degrees ↔ ∃ (d : σ →₀ ℕ), coeff d p ≠ 0 ∧ i ∈ d.support
source
theorem MvPolynomial.le_degrees_add_left {R : Type u} {σ : Type u_1} [CommSemiring R] {p q : MvPolynomial σ R} (h : Disjoint p.degrees q.degrees) :
p.degrees ≤ (p + q).degrees
source
theorem MvPolynomial.le_degrees_add_right {R : Type u} {σ : Type u_1} [CommSemiring R] {p q : MvPolynomial σ R} (h : Disjoint p.degrees q.degrees) :
q.degrees ≤ (p + q).degrees
source
theorem MvPolynomial.degrees_add_of_disjoint {R : Type u} {σ : Type u_1} [CommSemiring R] {p q : MvPolynomial σ R} [DecidableEq σ] (h : Disjoint p.degrees q.degrees) :
(p + q).degrees = p.degrees ∪ q.degrees
source
theorem MvPolynomial.degrees_map_le {R : Type u} {S : Type v} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} [CommSemiring S] {f : R →+* S} :
((map f) p).degrees ≤ p.degrees
source
theorem MvPolynomial.degrees_rename {R : Type u} {σ : Type u_1} {τ : Type u_2} [CommSemiring R] (f : σ → τ) (φ : MvPolynomial σ R) :
((rename f) φ).degrees ⊆ Multiset.map f φ.degrees
source
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) :
((map f) p).degrees = p.degrees
source
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) :
((rename f) p).degrees = Multiset.map f p.degrees

### `degreeOf` #

source
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

source
theorem MvPolynomial.degreeOf_def {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (n : σ) (p : MvPolynomial σ R) :
degreeOf n p = Multiset.count n p.degrees
source
theorem MvPolynomial.degreeOf_eq_sup {R : Type u} {σ : Type u_1} [CommSemiring R] (n : σ) (f : MvPolynomial σ R) :
degreeOf n f = f.support.sup fun (m : σ →₀ ℕ) => m n
source
theorem MvPolynomial.degreeOf_lt_iff {R : Type u} {σ : Type u_1} [CommSemiring R] {n : σ} {f : MvPolynomial σ R} {d : ℕ} (h : 0 < d) :
degreeOf n f < d ↔ ∀ m ∈ f.support, m n < d
source
theorem MvPolynomial.degreeOf_le_iff {R : Type u} {σ : Type u_1} [CommSemiring R] {n : σ} {f : MvPolynomial σ R} {d : ℕ} :
degreeOf n f ≤ d ↔ ∀ m ∈ f.support, m n ≤ d
source
@[simp]
theorem MvPolynomial.degreeOf_zero {R : Type u} {σ : Type u_1} [CommSemiring R] (n : σ) :
degreeOf n 0 = 0
source
@[simp]
theorem MvPolynomial.degreeOf_C {R : Type u} {σ : Type u_1} [CommSemiring R] (a : R) (x : σ) :
degreeOf x (C a) = 0
source
theorem MvPolynomial.degreeOf_X {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (i j : σ) [Nontrivial R] :
degreeOf i (X j) = if i = j then 1 else 0
source
theorem MvPolynomial.degreeOf_add_le {R : Type u} {σ : Type u_1} [CommSemiring R] (n : σ) (f g : MvPolynomial σ R) :
degreeOf n (f + g) ≤ max (degreeOf n f) (degreeOf n g)
source
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 ≤ degreeOf i f
source
theorem MvPolynomial.degreeOf_monomial_eq {R : Type u} {σ : Type u_1} [CommSemiring R] (s : σ →₀ ℕ) (i : σ) {a : R} (ha : a ≠ 0) :
degreeOf i ((monomial s) a) = s i
source
theorem MvPolynomial.degreeOf_mul_le {R : Type u} {σ : Type u_1} [CommSemiring R] (i : σ) (f g : MvPolynomial σ R) :
degreeOf i (f * g) ≤ degreeOf i f + degreeOf i g
source
theorem MvPolynomial.degreeOf_sum_le {R : Type u} {σ : Type u_1} [CommSemiring R] {ι : Type u_3} (i : σ) (s : Finset ι) (f : ι → MvPolynomial σ R) :
degreeOf i (∑ j ∈ s, f j) ≤ s.sup fun (j : ι) => degreeOf i (f j)
source
theorem MvPolynomial.degreeOf_prod_le {R : Type u} {σ : Type u_1} [CommSemiring R] {ι : Type u_3} (i : σ) (s : Finset ι) (f : ι → MvPolynomial σ R) :
degreeOf i (∏ j ∈ s, f j) ≤ ∑ j ∈ s, degreeOf i (f j)
source
theorem MvPolynomial.degreeOf_pow_le {R : Type u} {σ : Type u_1} [CommSemiring R] (i : σ) (p : MvPolynomial σ R) (n : ℕ) :
degreeOf i (p ^ n) ≤ n * degreeOf i p
source
theorem MvPolynomial.degreeOf_mul_X_of_ne {R : Type u} {σ : Type u_1} [CommSemiring R] {i j : σ} (f : MvPolynomial σ R) (h : i ≠ j) :
degreeOf i (f * X j) = degreeOf i f
source
theorem MvPolynomial.degreeOf_mul_X_self {R : Type u} {σ : Type u_1} [CommSemiring R] (j : σ) (f : MvPolynomial σ R) :
degreeOf j (f * X j) ≤ degreeOf j f + 1
source
theorem MvPolynomial.degreeOf_mul_X_eq_degreeOf_add_one_iff {R : Type u} {σ : Type u_1} [CommSemiring R] (j : σ) (f : MvPolynomial σ R) :
degreeOf j (f * X j) = degreeOf j f + 1 ↔ f ≠ 0
source
theorem MvPolynomial.degreeOf_C_mul_le {R : Type u} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) (i : σ) (c : R) :
degreeOf i (C c * p) ≤ degreeOf i p
source
theorem MvPolynomial.degreeOf_mul_C_le {R : Type u} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) (i : σ) (c : R) :
degreeOf i (p * C c) ≤ degreeOf i p
source
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 : σ) :
degreeOf (f i) ((rename f) p) = degreeOf i p

### `totalDegree` #

source
def MvPolynomial.totalDegree {R : Type u} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) :
ℕ

`totalDegree p` gives the maximum |s| over the monomials X^s in `p`

Equations

- p.totalDegree = p.support.sup fun (s : σ →₀ ℕ) => s.sum fun (x : σ) (e : ℕ) => e

Instances For

source
theorem MvPolynomial.totalDegree_eq {R : Type u} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) :
p.totalDegree = p.support.sup fun (m : σ →₀ ℕ) => (Finsupp.toMultiset m).card
source
theorem MvPolynomial.le_totalDegree {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} {s : σ →₀ ℕ} (h : s ∈ p.support) :
(s.sum fun (x : σ) (e : ℕ) => e) ≤ p.totalDegree
source
theorem MvPolynomial.totalDegree_le_degrees_card {R : Type u} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) :
p.totalDegree ≤ p.degrees.card
source
theorem MvPolynomial.totalDegree_le_of_support_subset {R : Type u} {σ : Type u_1} [CommSemiring R] {p q : MvPolynomial σ R} (h : p.support ⊆ q.support) :
p.totalDegree ≤ q.totalDegree
source
@[simp]
theorem MvPolynomial.totalDegree_C {R : Type u} {σ : Type u_1} [CommSemiring R] (a : R) :
(C a).totalDegree = 0
source
@[simp]
theorem MvPolynomial.totalDegree_zero {R : Type u} {σ : Type u_1} [CommSemiring R] :
totalDegree 0 = 0
source
@[simp]
theorem MvPolynomial.totalDegree_one {R : Type u} {σ : Type u_1} [CommSemiring R] :
totalDegree 1 = 0
source
@[simp]
theorem MvPolynomial.totalDegree_X {σ : Type u_1} {R : Type u_3} [CommSemiring R] [Nontrivial R] (s : σ) :
(X s).totalDegree = 1
source
theorem MvPolynomial.totalDegree_add {R : Type u} {σ : Type u_1} [CommSemiring R] (a b : MvPolynomial σ R) :
(a + b).totalDegree ≤ max a.totalDegree b.totalDegree
source
theorem MvPolynomial.totalDegree_add_eq_left_of_totalDegree_lt {R : Type u} {σ : Type u_1} [CommSemiring R] {p q : MvPolynomial σ R} (h : q.totalDegree < p.totalDegree) :
(p + q).totalDegree = p.totalDegree
source
theorem MvPolynomial.totalDegree_add_eq_right_of_totalDegree_lt {R : Type u} {σ : Type u_1} [CommSemiring R] {p q : MvPolynomial σ R} (h : q.totalDegree < p.totalDegree) :
(q + p).totalDegree = p.totalDegree
source
theorem MvPolynomial.totalDegree_mul {R : Type u} {σ : Type u_1} [CommSemiring R] (a b : MvPolynomial σ R) :
(a * b).totalDegree ≤ a.totalDegree + b.totalDegree
source
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) :
(a • f).totalDegree ≤ f.totalDegree
source
theorem MvPolynomial.totalDegree_pow {R : Type u} {σ : Type u_1} [CommSemiring R] (a : MvPolynomial σ R) (n : ℕ) :
(a ^ n).totalDegree ≤ n * a.totalDegree
source
@[simp]
theorem MvPolynomial.totalDegree_monomial {R : Type u} {σ : Type u_1} [CommSemiring R] (s : σ →₀ ℕ) {c : R} (hc : c ≠ 0) :
((monomial s) c).totalDegree = s.sum fun (x : σ) (e : ℕ) => e
source
theorem MvPolynomial.totalDegree_monomial_le {R : Type u} {σ : Type u_1} [CommSemiring R] (s : σ →₀ ℕ) (c : R) :
((monomial s) c).totalDegree ≤ s.sum fun (x : σ) => id
source
@[simp]
theorem MvPolynomial.totalDegree_X_pow {R : Type u} {σ : Type u_1} [CommSemiring R] [Nontrivial R] (s : σ) (n : ℕ) :
(X s ^ n).totalDegree = n
source
theorem MvPolynomial.totalDegree_list_prod {R : Type u} {σ : Type u_1} [CommSemiring R] (l : List (MvPolynomial σ R)) :
l.prod.totalDegree ≤ (List.map totalDegree l).sum
source
theorem MvPolynomial.totalDegree_multiset_prod {R : Type u} {σ : Type u_1} [CommSemiring R] (s : Multiset (MvPolynomial σ R)) :
s.prod.totalDegree ≤ (Multiset.map totalDegree s).sum
source
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 ≤ ∑ i ∈ s, (f i).totalDegree
source
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
source
theorem MvPolynomial.totalDegree_finsetSum_le {R : Type u} {σ : Type u_1} [CommSemiring R] {ι : Type u_3} {s : Finset ι} {f : ι → MvPolynomial σ R} {d : ℕ} (hf : ∀ i ∈ s, (f i).totalDegree ≤ d) :
(s.sum f).totalDegree ≤ d
source
theorem MvPolynomial.degreeOf_le_totalDegree {R : Type u} {σ : Type u_1} [CommSemiring R] (f : MvPolynomial σ R) (i : σ) :
degreeOf i f ≤ f.totalDegree
source
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
source
theorem MvPolynomial.coeff_eq_zero_of_totalDegree_lt {R : Type u} {σ : Type u_1} [CommSemiring R] {f : MvPolynomial σ R} {d : σ →₀ ℕ} (h : f.totalDegree < ∑ i ∈ d.support, d i) :
coeff d f = 0
source
theorem MvPolynomial.totalDegree_eq_zero_iff_eq_C {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} :
p.totalDegree = 0 ↔ p = C (coeff 0 p)
source
theorem MvPolynomial.totalDegree_rename_le {R : Type u} {σ : Type u_1} {τ : Type u_2} [CommSemiring R] (f : σ → τ) (p : MvPolynomial σ R) :
((rename f) p).totalDegree ≤ p.totalDegree
source
theorem MvPolynomial.totalDegree_renameEquiv {R : Type u} {σ : Type u_1} {τ : Type u_2} [CommSemiring R] (f : σ ≃ τ) (p : MvPolynomial σ R) :
((renameEquiv R f) p).totalDegree = p.totalDegree
source
def MvPolynomial.degreesLE (R : Type u) (σ : Type u_1) [CommSemiring R] (s : Multiset σ) :
Submodule R (MvPolynomial σ R)

The submodule of multivariate polynomials of degrees bounded by a monomial `s`.

Equations

- MvPolynomial.degreesLE R σ s = { carrier := {p : MvPolynomial σ R | p.degrees ≤ s}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

Instances For

source
@[simp]
theorem MvPolynomial.mem_degreesLE {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} {s : Multiset σ} :
p ∈ degreesLE R σ s ↔ p.degrees ≤ s
source
theorem MvPolynomial.degreesLE_add {R : Type u} {σ : Type u_1} [CommSemiring R] (s t : Multiset σ) :
degreesLE R σ (s + t) = degreesLE R σ s * degreesLE R σ t
source
@[simp]
theorem MvPolynomial.degreesLE_zero {R : Type u} {σ : Type u_1} [CommSemiring R] :
degreesLE R σ 0 = 1
source
theorem MvPolynomial.degreesLE_nsmul {R : Type u} {σ : Type u_1} [CommSemiring R] (s : Multiset σ) (n : ℕ) :
degreesLE R σ (n • s) = degreesLE R σ s ^ n