Mathlib.Algebra.Polynomial.Degree.Support

Polynomial.supDegree_eq_natDegree theorem

(p : R[X]) : p.toFinsupp.supDegree id = p.natDegree

Full source

theorem supDegree_eq_natDegree (p : R[X]) : p.toFinsupp.supDegree id = p.natDegree := by
  obtain rfl|h := eq_or_ne p 0
  · simp
  apply WithBot.coe_injective
  rw [← AddMonoidAlgebra.supDegree_withBot_some_comp, Function.comp_id, supDegree_eq_degree,
    degree_eq_natDegree h, Nat.cast_withBot]
  rwa [support_toFinsupp, nonempty_iff_ne_empty, Ne, support_eq_empty]

Equality of Sup-Degree and Natural Degree for Polynomials: $\text{supDegree}(p) = \text{natDegree}(p)$

Informal description

For any polynomial $p \in R[X]$, the supremum degree of $p$ (viewed as an element of the additive monoid algebra $R[\mathbb{N}]$) with respect to the identity function equals the natural degree of $p$. In other words, when considering $p$ as a formal sum in $R[\mathbb{N}]$, the highest exponent with a nonzero coefficient (its sup-degree) coincides with the natural degree of $p$ (the highest power of $X$ with a nonzero coefficient).

Polynomial.le_natDegree_of_mem_supp theorem

(a : ℕ) : a ∈ p.support → a ≤ natDegree p

Full source

theorem le_natDegree_of_mem_supp (a : ℕ) : a ∈ p.support → a ≤ natDegree p :=
  le_natDegree_of_ne_zerole_natDegree_of_ne_zero ∘ mem_support_iff.mp

Support Elements Bounded by Natural Degree in Polynomials

Informal description

For any polynomial $p \in R[X]$ and natural number $a$, if $a$ is in the support of $p$ (i.e., the coefficient of $X^a$ in $p$ is nonzero), then $a$ is less than or equal to the natural degree of $p$.

Polynomial.supp_subset_range theorem

(h : natDegree p < m) : p.support ⊆ Finset.range m

Full source

theorem supp_subset_range (h : natDegree p < m) : p.support ⊆ Finset.range m := fun _n hn =>
  mem_range.2 <| (le_natDegree_of_mem_supp _ hn).trans_lt h

Support of Polynomial with Bounded Degree is Contained in Initial Segment

Informal description

For a polynomial $p \in R[X]$ and a natural number $m$, if the natural degree of $p$ is less than $m$, then the support of $p$ is a subset of the finite set $\{0, 1, \ldots, m-1\}$.

Polynomial.supp_subset_range_natDegree_succ theorem

: p.support ⊆ Finset.range (natDegree p + 1)

Full source

theorem supp_subset_range_natDegree_succ : p.support ⊆ Finset.range (natDegree p + 1) :=
  supp_subset_range (Nat.lt_succ_self _)

Support of Polynomial is Contained in Initial Segment up to Degree Plus One

Informal description

For any polynomial $p \in R[X]$, the support of $p$ is a subset of the finite set $\{0, 1, \ldots, \text{natDegree}(p)\}$.

Polynomial.as_sum_support theorem

(p : R[X]) : p = ∑ i ∈ p.support, monomial i (p.coeff i)

Full source

theorem as_sum_support (p : R[X]) : p = ∑ i ∈ p.support, monomial i (p.coeff i) :=
  (sum_monomial_eq p).symm

Polynomial as Sum over Support

Informal description

For any polynomial $p \in R[X]$, $p$ can be expressed as the sum of its monomial terms over its support: \[ p = \sum_{i \in \text{supp}(p)} a_i X^i \] where $\text{supp}(p) = \{i \in \mathbb{N} \mid a_i \neq 0\}$ is the set of exponents with nonzero coefficients in $p$, and $a_i$ is the coefficient of $X^i$ in $p$.

Polynomial.as_sum_support_C_mul_X_pow theorem

(p : R[X]) : p = ∑ i ∈ p.support, C (p.coeff i) * X ^ i

Full source

theorem as_sum_support_C_mul_X_pow (p : R[X]) : p = ∑ i ∈ p.support, C (p.coeff i) * X ^ i :=
  _root_.trans p.as_sum_support <| by simp only [C_mul_X_pow_eq_monomial]

Polynomial as Sum of Monomials over Support

Informal description

For any polynomial $p \in R[X]$, $p$ can be expressed as the sum of its monomial terms over its support: \[ p = \sum_{i \in \text{supp}(p)} a_i X^i \] where $\text{supp}(p) = \{i \in \mathbb{N} \mid a_i \neq 0\}$ is the set of exponents with nonzero coefficients in $p$, and $a_i$ is the coefficient of $X^i$ in $p$.

Polynomial.sum_over_range' theorem

 [AddCommMonoid S] (p : R[X]) {f : ℕ → R → S} (h : ∀ n, f n 0 = 0) (n : ℕ) (w : p.natDegree < n) :
  p.sum f = ∑ a ∈ range n, f a (coeff p a)

Full source

/-- We can reexpress a sum over `p.support` as a sum over `range n`,
for any `n` satisfying `p.natDegree < n`.
-/
theorem sum_over_range' [AddCommMonoid S] (p : R[X]) {f : ℕ → R → S} (h : ∀ n, f n 0 = 0) (n : ℕ)
    (w : p.natDegree < n) : p.sum f = ∑ a ∈ range n, f a (coeff p a) := by
  rcases p with ⟨⟩
  have := supp_subset_range w
  simp only [Polynomial.sum, support, coeff, natDegree, degree] at this ⊢
  exact Finsupp.sum_of_support_subset _ this _ fun n _hn => h n

Sum over polynomial support equals sum over range when degree is bounded

Informal description

Let $p \in R[X]$ be a polynomial over a semiring $R$, and let $S$ be an additive commutative monoid. Given a function $f : \mathbb{N} \to R \to S$ such that $f(n, 0) = 0$ for all $n \in \mathbb{N}$, and a natural number $n$ satisfying $\text{natDegree}(p) < n$, the sum over the support of $p$ can be expressed as a sum over the range $\{0, \dots, n-1\}$. That is, \[ \sum_{i \in \text{support}(p)} f(i, \text{coeff}(p, i)) = \sum_{a=0}^{n-1} f(a, \text{coeff}(p, a)). \]

Polynomial.sum_over_range theorem

 [AddCommMonoid S] (p : R[X]) {f : ℕ → R → S} (h : ∀ n, f n 0 = 0) :
  p.sum f = ∑ a ∈ range (p.natDegree + 1), f a (coeff p a)

Full source

/-- We can reexpress a sum over `p.support` as a sum over `range (p.natDegree + 1)`.
-/
theorem sum_over_range [AddCommMonoid S] (p : R[X]) {f : ℕ → R → S} (h : ∀ n, f n 0 = 0) :
    p.sum f = ∑ a ∈ range (p.natDegree + 1), f a (coeff p a) :=
  sum_over_range' p h (p.natDegree + 1) (lt_add_one _)

Polynomial Sum over Support Equals Sum over Degree Range

Informal description

Let $R$ be a semiring and $S$ an additive commutative monoid. Given a polynomial $p \in R[X]$ and a function $f : \mathbb{N} \to R \to S$ such that $f(n, 0) = 0$ for all $n \in \mathbb{N}$, the sum over the support of $p$ can be expressed as a sum over the range $\{0, \dots, \text{natDegree}(p)\}$. That is, \[ \sum_{i \in \text{support}(p)} f(i, \text{coeff}(p, i)) = \sum_{a=0}^{\text{natDegree}(p)} f(a, \text{coeff}(p, a)). \]

Polynomial.sum_fin theorem

 [AddCommMonoid S] (f : ℕ → R → S) (hf : ∀ i, f i 0 = 0) {n : ℕ} {p : R[X]} (hn : p.degree < n) :
  (∑ i : Fin n, f i (p.coeff i)) = p.sum f

Full source

theorem sum_fin [AddCommMonoid S] (f : ℕ → R → S) (hf : ∀ i, f i 0 = 0) {n : ℕ} {p : R[X]}
    (hn : p.degree < n) : (∑ i : Fin n, f i (p.coeff i)) = p.sum f := by
  by_cases hp : p = 0
  · rw [hp, sum_zero_index, Finset.sum_eq_zero]
    intro i _
    exact hf i
  rw [sum_over_range' _ hf n ((natDegree_lt_iff_degree_lt hp).mpr hn),
    Fin.sum_univ_eq_sum_range fun i => f i (p.coeff i)]

Equality of polynomial sums over finite support and range when degree is bounded

Informal description

Let $R$ be a semiring, $S$ an additive commutative monoid, and $f \colon \mathbb{N} \to R \to S$ a function such that $f(i, 0) = 0$ for all $i \in \mathbb{N}$. For any polynomial $p \in R[X]$ and natural number $n$ satisfying $\deg(p) < n$, the sum over the first $n$ coefficients of $p$ equals the sum over its support: \[ \sum_{i=0}^{n-1} f(i, [X^i]p) = \sum_{i \in \operatorname{supp}(p)} f(i, [X^i]p). \]

Polynomial.as_sum_range' theorem

(p : R[X]) (n : ℕ) (w : p.natDegree < n) : p = ∑ i ∈ range n, monomial i (coeff p i)

Full source

theorem as_sum_range' (p : R[X]) (n : ℕ) (w : p.natDegree < n) :
    p = ∑ i ∈ range n, monomial i (coeff p i) :=
  p.sum_monomial_eq.symm.trans <| p.sum_over_range' monomial_zero_right _ w

Polynomial as Sum over Range when Degree is Bounded

Informal description

Let $p \in R[X]$ be a polynomial over a semiring $R$, and let $n \in \mathbb{N}$ be a natural number such that the degree of $p$ is less than $n$. Then $p$ can be expressed as the sum of monomials over the range $\{0, \dots, n-1\}$: \[ p = \sum_{i=0}^{n-1} a_i X^i, \] where $a_i$ is the coefficient of $X^i$ in $p$.

Polynomial.as_sum_range theorem

(p : R[X]) : p = ∑ i ∈ range (p.natDegree + 1), monomial i (coeff p i)

Full source

theorem as_sum_range (p : R[X]) : p = ∑ i ∈ range (p.natDegree + 1), monomial i (coeff p i) :=
  p.sum_monomial_eq.symm.trans <| p.sum_over_range <| monomial_zero_right

Polynomial as Sum over Degree Range

Informal description

For any polynomial $p \in R[X]$ over a semiring $R$, $p$ can be expressed as the sum of monomials over the range $\{0, \dots, \deg(p)\}$: \[ p = \sum_{i=0}^{\deg(p)} a_i X^i, \] where $a_i$ is the coefficient of $X^i$ in $p$.

Polynomial.as_sum_range_C_mul_X_pow theorem

(p : R[X]) : p = ∑ i ∈ range (p.natDegree + 1), C (coeff p i) * X ^ i

Full source

theorem as_sum_range_C_mul_X_pow (p : R[X]) :
    p = ∑ i ∈ range (p.natDegree + 1), C (coeff p i) * X ^ i :=
  p.as_sum_range.trans <| by simp only [C_mul_X_pow_eq_monomial]

Polynomial Expansion in Terms of Coefficients and Powers of $X$

Informal description

For any polynomial $p \in R[X]$ over a semiring $R$, $p$ can be expressed as the sum of terms $C(a_i) \cdot X^i$ over the range $\{0, \dots, \deg(p)\}$, where $a_i$ is the coefficient of $X^i$ in $p$: \[ p = \sum_{i=0}^{\deg(p)} a_i X^i. \]

Polynomial.mem_support_C_mul_X_pow theorem

{n a : ℕ} {c : R} (h : a ∈ support (C c * X ^ n)) : a = n

Full source

theorem mem_support_C_mul_X_pow {n a : ℕ} {c : R} (h : a ∈ support (C c * X ^ n)) : a = n :=
  mem_singleton.1 <| support_C_mul_X_pow' n c h

Support of $c X^n$ is exactly $\{n\}$ when $c \neq 0$

Informal description

For any natural numbers $n$ and $a$, and any coefficient $c$ in a semiring $R$, if $a$ belongs to the support of the polynomial $c X^n$, then $a = n$.

Polynomial.card_support_C_mul_X_pow_le_one theorem

{c : R} {n : ℕ} : #(support (C c * X ^ n)) ≤ 1

Full source

theorem card_support_C_mul_X_pow_le_one {c : R} {n : ℕ} : #(support (C c * X ^ n)) ≤ 1 := by
  rw [← card_singleton n]
  apply card_le_card (support_C_mul_X_pow' n c)

Support Cardinality Bound for Monomials: $\#\text{supp}(c X^n) \leq 1$

Informal description

For any coefficient $c$ in a semiring $R$ and any natural number $n$, the support of the polynomial $c X^n$ has cardinality at most 1. In other words, the polynomial $c X^n$ has at most one nonzero coefficient.

Polynomial.card_supp_le_succ_natDegree theorem

(p : R[X]) : #p.support ≤ p.natDegree + 1

Full source

theorem card_supp_le_succ_natDegree (p : R[X]) : #p.support ≤ p.natDegree + 1 := by
  rw [← Finset.card_range (p.natDegree + 1)]
  exact Finset.card_le_card supp_subset_range_natDegree_succ

Cardinality Bound for Polynomial Support: $\#\text{supp}(p) \leq \text{natDegree}(p) + 1$

Informal description

For any polynomial $p \in R[X]$, the cardinality of its support (the set of exponents with nonzero coefficients) is at most its natural degree plus one, i.e., $\#\text{supp}(p) \leq \text{natDegree}(p) + 1$.

Polynomial.le_degree_of_mem_supp theorem

(a : ℕ) : a ∈ p.support → ↑a ≤ degree p

Full source

theorem le_degree_of_mem_supp (a : ℕ) : a ∈ p.support → ↑a ≤ degree p :=
  le_degree_of_ne_zerole_degree_of_ne_zero ∘ mem_support_iff.mp

Exponents in Support are Bounded by Degree

Informal description

For any polynomial $p \in R[X]$ and natural number $a$, if $a$ is in the support of $p$ (i.e., the coefficient of $X^a$ in $p$ is nonzero), then $a$ is less than or equal to the degree of $p$ (where the degree is considered in $\mathbb{N} \cup \{\bot\}$ with $\bot$ representing $-\infty$).

Polynomial.nonempty_support_iff theorem

: p.support.Nonempty ↔ p ≠ 0

Full source

theorem nonempty_support_iff : p.support.Nonempty ↔ p ≠ 0 := by
  rw [Ne, nonempty_iff_ne_empty, Ne, ← support_eq_empty]

Characterization of Nonzero Polynomials via Nonempty Support

Informal description

For a polynomial $p \in R[X]$, the support of $p$ is nonempty if and only if $p$ is not the zero polynomial. That is, $p$ has at least one nonzero coefficient if and only if $p \neq 0$.

Polynomial.natDegree_mem_support_of_nonzero theorem

(H : p ≠ 0) : p.natDegree ∈ p.support

Full source

theorem natDegree_mem_support_of_nonzero (H : p ≠ 0) : p.natDegree ∈ p.support := by
  rw [mem_support_iff]
  exact (not_congr leadingCoeff_eq_zero).mpr H

Nonzero Polynomials Have Nonzero Leading Coefficient

Informal description

For any nonzero polynomial $p \in R[X]$, the natural degree of $p$ (denoted $\mathrm{natDegree}(p)$) is an element of the support of $p$, i.e., the coefficient of $X^{\mathrm{natDegree}(p)}$ in $p$ is nonzero.

Polynomial.natDegree_eq_support_max' theorem

(h : p ≠ 0) : p.natDegree = p.support.max' (nonempty_support_iff.mpr h)

Full source

theorem natDegree_eq_support_max' (h : p ≠ 0) :
    p.natDegree = p.support.max' (nonempty_support_iff.mpr h) :=
  (le_max' _ _ <| natDegree_mem_support_of_nonzero h).antisymm <|
    max'_le _ _ _ le_natDegree_of_mem_supp

Natural Degree Equals Maximum Support Exponent for Nonzero Polynomials

Informal description

For any nonzero polynomial $p \in R[X]$, the natural degree of $p$ is equal to the maximum element of its support. That is, $\mathrm{natDegree}(p) = \max'(\mathrm{support}(p))$, where $\mathrm{support}(p)$ is the set of exponents with nonzero coefficients in $p$.

Main results