doc-next-gen

Mathlib.Algebra.MonoidAlgebra.Degree

Module docstring

{"# Lemmas about the sup and inf of the support of AddMonoidAlgebra

TODO

The current plan is to state and prove lemmas about Finset.sup (Finsupp.support f) D with a \"generic\" degree/weight function D from the grading Type A to a somewhat ordered Type B.

Next, the general lemmas get specialized for some yet-to-be-defined degrees. ","# sup-degree and inf-degree of an AddMonoidAlgebra

Let R be a semiring and let A be a SemilatticeSup. For an element f : R[A], this file defines * AddMonoidAlgebra.supDegree: the sup-degree taking values in WithBot A, * AddMonoidAlgebra.infDegree: the inf-degree taking values in WithTop A.

If the grading type A is a linearly ordered additive monoid, then these two notions of degree coincide with the standard one: * the sup-degree is the maximum of the exponents of the monomials that appear with non-zero coefficient in f, or ⊥, if f = 0; * the inf-degree is the minimum of the exponents of the monomials that appear with non-zero coefficient in f, or ⊤, if f = 0.

The main results are * AddMonoidAlgebra.supDegree_mul_le: the sup-degree of a product is at most the sum of the sup-degrees, * AddMonoidAlgebra.le_infDegree_mul: the inf-degree of a product is at least the sum of the inf-degrees, * AddMonoidAlgebra.supDegree_add_le: the sup-degree of a sum is at most the sup of the sup-degrees, * AddMonoidAlgebra.le_infDegree_add: the inf-degree of a sum is at least the inf of the inf-degrees.

Implementation notes

The current plan is to state and prove lemmas about Finset.sup (Finsupp.support f) D with a \"generic\" degree/weight function D from the grading Type A to a somewhat ordered Type B. Next, the general lemmas get specialized twice: * once for supDegree (essentially a simple application) and * once for infDegree (a simple application, via OrderDual).

These final lemmas are the ones that likely get used the most. The generic lemmas about Finset.support.sup may not be used directly much outside of this file. To see this in action, you can look at the triple (sup_support_mul_le, maxDegree_mul_le, le_minDegree_mul). ","In this section, we use degb and degt to denote \"degree functions\" on A with values in a type with bot or top respectively. ","### Shorthands for special cases Note that these definitions are reducible, in order to make it easier to apply the more generic lemmas above. "}

AddMonoidAlgebra.sup_support_mul_le theorem
{degb : A → B} (degbm : ∀ {a b}, degb (a + b) ≤ degb a + degb b) (f g : R[A]) : (f * g).support.sup degb ≤ f.support.sup degb + g.support.sup degb
Full source 
theorem sup_support_mul_le {degb : A → B} (degbm : ∀ {a b}, degb (a + b) ≤ degb a + degb b)
    (f g : R[A]) :
    (f * g).support.sup degb ≤ f.support.sup degb + g.support.sup degb := by
  classical
  exact (Finset.sup_mono <| support_mul _ _).trans <| Finset.sup_add_le.2 fun _fd fds _gd gds ↦
    degbm.trans <| add_le_add (Finset.le_sup fds) (Finset.le_sup gds)
Subadditivity of Sup-Degree under Multiplication in Additive Monoid Algebra
Informal description
Let $R$ be a semiring and $A$ a join-semilattice. Given a function $\operatorname{degb} \colon A \to B$ that satisfies the subadditivity condition $\operatorname{degb}(a + b) \leq \operatorname{degb}(a) + \operatorname{degb}(b)$ for all $a, b \in A$, then for any two elements $f, g \in R[A]$, the supremum of $\operatorname{degb}$ over the support of their product is bounded by the sum of the suprema over their individual supports: \[ \sup_{x \in \operatorname{supp}(f * g)} \operatorname{degb}(x) \leq \sup_{x \in \operatorname{supp}(f)} \operatorname{degb}(x) + \sup_{x \in \operatorname{supp}(g)} \operatorname{degb}(x). \]
AddMonoidAlgebra.le_inf_support_mul theorem
{degt : A → T} (degtm : ∀ {a b}, degt a + degt b ≤ degt (a + b)) (f g : R[A]) : f.support.inf degt + g.support.inf degt ≤ (f * g).support.inf degt
Full source 
theorem le_inf_support_mul {degt : A → T} (degtm : ∀ {a b}, degt a + degt b ≤ degt (a + b))
    (f g : R[A]) :
    f.support.inf degt + g.support.inf degt ≤ (f * g).support.inf degt :=
  sup_support_mul_le (B := Tᵒᵈ) degtm f g
Superadditivity of Inf-Degree under Multiplication in Additive Monoid Algebra
Informal description
Let $R$ be a semiring and $A$ a meet-semilattice. Given a function $\operatorname{degt} \colon A \to T$ that satisfies the superadditivity condition $\operatorname{degt}(a) + \operatorname{degt}(b) \leq \operatorname{degt}(a + b)$ for all $a, b \in A$, then for any two elements $f, g \in R[A]$, the sum of the infima of $\operatorname{degt}$ over their individual supports is bounded by the infimum over the support of their product: \[ \inf_{x \in \operatorname{supp}(f)} \operatorname{degt}(x) + \inf_{x \in \operatorname{supp}(g)} \operatorname{degt}(x) \leq \inf_{x \in \operatorname{supp}(f * g)} \operatorname{degt}(x). \]
AddMonoidAlgebra.sup_support_list_prod_le theorem
(degb0 : degb 0 ≤ 0) (degbm : ∀ a b, degb (a + b) ≤ degb a + degb b) : ∀ l : List R[A], l.prod.support.sup degb ≤ (l.map fun f : R[A] => f.support.sup degb).sum
Full source 
theorem sup_support_list_prod_le (degb0 : degb 0 ≤ 0)
    (degbm : ∀ a b, degb (a + b) ≤ degb a + degb b) :
    ∀ l : List R[A],
      l.prod.support.sup degb ≤ (l.map fun f : R[A] => f.support.sup degb).sum
  | [] => by
    rw [List.map_nil, Finset.sup_le_iff, List.prod_nil, List.sum_nil]
    exact fun a ha => by rwa [Finset.mem_singleton.mp (Finsupp.support_single_subset ha)]
  | f::fs => by
    rw [List.prod_cons, List.map_cons, List.sum_cons]
    exact (sup_support_mul_le (@fun a b => degbm a b) _ _).trans
        (add_le_add_left (sup_support_list_prod_le degb0 degbm fs) _)
Subadditivity of Sup-Degree under List Product in Additive Monoid Algebra
Informal description
Let $R$ be a semiring and $A$ a join-semilattice. Given a function $\operatorname{degb} \colon A \to B$ that satisfies: 1. $\operatorname{degb}(0) \leq 0$, and 2. $\operatorname{degb}(a + b) \leq \operatorname{degb}(a) + \operatorname{degb}(b)$ for all $a, b \in A$, then for any list $l$ of elements in the additive monoid algebra $R[A]$, the supremum of $\operatorname{degb}$ over the support of the product of elements in $l$ is bounded by the sum of the suprema over their individual supports: \[ \sup_{x \in \operatorname{supp}(\prod l)} \operatorname{degb}(x) \leq \sum_{f \in l} \left( \sup_{x \in \operatorname{supp}(f)} \operatorname{degb}(x) \right). \]
AddMonoidAlgebra.le_inf_support_list_prod theorem
(degt0 : 0 ≤ degt 0) (degtm : ∀ a b, degt a + degt b ≤ degt (a + b)) (l : List R[A]) : (l.map fun f : R[A] => f.support.inf degt).sum ≤ l.prod.support.inf degt
Full source 
theorem le_inf_support_list_prod (degt0 : 0 ≤ degt 0)
    (degtm : ∀ a b, degt a + degt b ≤ degt (a + b)) (l : List R[A]) :
    (l.map fun f : R[A] => f.support.inf degt).sum ≤ l.prod.support.inf degt := by
  refine OrderDual.ofDual_le_ofDual.mpr ?_
  refine sup_support_list_prod_le ?_ ?_ l
  · refine (OrderDual.ofDual_le_ofDual.mp ?_)
    exact degt0
  · refine (fun a b => OrderDual.ofDual_le_ofDual.mp ?_)
    exact degtm a b
Superadditivity of Inf-Degree under List Product in Additive Monoid Algebra
Informal description
Let $R$ be a semiring and $A$ a meet-semilattice. Given a function $\operatorname{degt} \colon A \to T$ that satisfies: 1. $0 \leq \operatorname{degt}(0)$, and 2. $\operatorname{degt}(a) + \operatorname{degt}(b) \leq \operatorname{degt}(a + b)$ for all $a, b \in A$, then for any list $l$ of elements in the additive monoid algebra $R[A]$, the sum of the infima of $\operatorname{degt}$ over their individual supports is bounded by the infimum over the support of their product: \[ \sum_{f \in l} \left( \inf_{x \in \operatorname{supp}(f)} \operatorname{degt}(x) \right) \leq \inf_{x \in \operatorname{supp}(\prod l)} \operatorname{degt}(x). \]
AddMonoidAlgebra.sup_support_pow_le theorem
(degb0 : degb 0 ≤ 0) (degbm : ∀ a b, degb (a + b) ≤ degb a + degb b) (n : ℕ) (f : R[A]) : (f ^ n).support.sup degb ≤ n • f.support.sup degb
Full source 
theorem sup_support_pow_le (degb0 : degb 0 ≤ 0) (degbm : ∀ a b, degb (a + b) ≤ degb a + degb b)
    (n : ℕ) (f : R[A]) : (f ^ n).support.sup degb ≤ n • f.support.sup degb := by
  rw [← List.prod_replicate, ← List.sum_replicate]
  refine (sup_support_list_prod_le degb0 degbm _).trans_eq ?_
  rw [List.map_replicate]
Subadditivity of Sup-Degree under Power in Additive Monoid Algebra
Informal description
Let $R$ be a semiring and $A$ a join-semilattice. Given a function $\operatorname{degb} \colon A \to B$ that satisfies: 1. $\operatorname{degb}(0) \leq 0$, and 2. $\operatorname{degb}(a + b) \leq \operatorname{degb}(a) + \operatorname{degb}(b)$ for all $a, b \in A$, then for any natural number $n$ and any element $f$ in the additive monoid algebra $R[A]$, the supremum of $\operatorname{degb}$ over the support of $f^n$ is bounded by $n$ times the supremum over the support of $f$: \[ \sup_{x \in \operatorname{supp}(f^n)} \operatorname{degb}(x) \leq n \cdot \left( \sup_{x \in \operatorname{supp}(f)} \operatorname{degb}(x) \right). \]
AddMonoidAlgebra.le_inf_support_pow theorem
(degt0 : 0 ≤ degt 0) (degtm : ∀ a b, degt a + degt b ≤ degt (a + b)) (n : ℕ) (f : R[A]) : n • f.support.inf degt ≤ (f ^ n).support.inf degt
Full source 
theorem le_inf_support_pow (degt0 : 0 ≤ degt 0) (degtm : ∀ a b, degt a + degt b ≤ degt (a + b))
    (n : ℕ) (f : R[A]) : n • f.support.inf degt ≤ (f ^ n).support.inf degt := by
  refine OrderDual.ofDual_le_ofDual.mpr <| sup_support_pow_le (OrderDual.ofDual_le_ofDual.mp ?_)
      (fun a b => OrderDual.ofDual_le_ofDual.mp ?_) n f
  · exact degt0
  · exact degtm _ _
Superadditivity of Inf-Degree under Power in Additive Monoid Algebra
Informal description
Let $R$ be a semiring and $A$ a meet-semilattice. Given a function $\operatorname{degt} \colon A \to T$ that satisfies: 1. $0 \leq \operatorname{degt}(0)$, and 2. $\operatorname{degt}(a) + \operatorname{degt}(b) \leq \operatorname{degt}(a + b)$ for all $a, b \in A$, then for any natural number $n$ and any element $f$ in the additive monoid algebra $R[A]$, the infimum of $\operatorname{degt}$ over the support of $f^n$ is bounded below by $n$ times the infimum over the support of $f$: \[ n \cdot \left( \inf_{x \in \operatorname{supp}(f)} \operatorname{degt}(x) \right) \leq \inf_{x \in \operatorname{supp}(f^n)} \operatorname{degt}(x). \]
AddMonoidAlgebra.sup_support_multiset_prod_le theorem
(degb0 : degb 0 ≤ 0) (degbm : ∀ a b, degb (a + b) ≤ degb a + degb b) (m : Multiset R[A]) : m.prod.support.sup degb ≤ (m.map fun f : R[A] => f.support.sup degb).sum
Full source 
theorem sup_support_multiset_prod_le (degb0 : degb 0 ≤ 0)
    (degbm : ∀ a b, degb (a + b) ≤ degb a + degb b) (m : Multiset R[A]) :
    m.prod.support.sup degb ≤ (m.map fun f : R[A] => f.support.sup degb).sum := by
  induction m using Quot.inductionOn
  rw [Multiset.quot_mk_to_coe'', Multiset.map_coe, Multiset.sum_coe, Multiset.prod_coe]
  exact sup_support_list_prod_le degb0 degbm _
Subadditivity of Sup-Degree under Multiset Product in Additive Monoid Algebra
Informal description
Let $R$ be a semiring and $A$ a join-semilattice. Given a function $\operatorname{degb} \colon A \to B$ that satisfies: 1. $\operatorname{degb}(0) \leq 0$, and 2. $\operatorname{degb}(a + b) \leq \operatorname{degb}(a) + \operatorname{degb}(b)$ for all $a, b \in A$, then for any multiset $m$ of elements in the additive monoid algebra $R[A]$, the supremum of $\operatorname{degb}$ over the support of the product of elements in $m$ is bounded by the sum of the suprema over their individual supports: \[ \sup_{x \in \operatorname{supp}(\prod m)} \operatorname{degb}(x) \leq \sum_{f \in m} \left( \sup_{x \in \operatorname{supp}(f)} \operatorname{degb}(x) \right). \]
AddMonoidAlgebra.le_inf_support_multiset_prod theorem
(degt0 : 0 ≤ degt 0) (degtm : ∀ a b, degt a + degt b ≤ degt (a + b)) (m : Multiset R[A]) : (m.map fun f : R[A] => f.support.inf degt).sum ≤ m.prod.support.inf degt
Full source 
theorem le_inf_support_multiset_prod (degt0 : 0 ≤ degt 0)
    (degtm : ∀ a b, degt a + degt b ≤ degt (a + b)) (m : Multiset R[A]) :
    (m.map fun f : R[A] => f.support.inf degt).sum ≤ m.prod.support.inf degt := by
  refine OrderDual.ofDual_le_ofDual.mpr <|
    sup_support_multiset_prod_le (OrderDual.ofDual_le_ofDual.mp ?_)
      (fun a b => OrderDual.ofDual_le_ofDual.mp ?_) m
  · exact degt0
  · exact degtm _ _
Superadditivity of Inf-Degree under Multiset Product in Additive Monoid Algebra
Informal description
Let $R$ be a semiring and $A$ a meet-semilattice. Given a function $\operatorname{degt} \colon A \to T$ that satisfies: 1. $0 \leq \operatorname{degt}(0)$, and 2. $\operatorname{degt}(a) + \operatorname{degt}(b) \leq \operatorname{degt}(a + b)$ for all $a, b \in A$, then for any multiset $m$ of elements in the additive monoid algebra $R[A]$, the infimum of $\operatorname{degt}$ over the support of the product of elements in $m$ is bounded below by the sum of the infima over their individual supports: \[ \sum_{f \in m} \left( \inf_{x \in \operatorname{supp}(f)} \operatorname{degt}(x) \right) \leq \inf_{x \in \operatorname{supp}(\prod m)} \operatorname{degt}(x). \]
AddMonoidAlgebra.sup_support_finset_prod_le theorem
(degb0 : degb 0 ≤ 0) (degbm : ∀ a b, degb (a + b) ≤ degb a + degb b) (s : Finset ι) (f : ι → R[A]) : (∏ i ∈ s, f i).support.sup degb ≤ ∑ i ∈ s, (f i).support.sup degb
Full source 
theorem sup_support_finset_prod_le (degb0 : degb 0 ≤ 0)
    (degbm : ∀ a b, degb (a + b) ≤ degb a + degb b) (s : Finset ι) (f : ι → R[A]) :
    (∏ i ∈ s, f i).support.sup degb ≤ ∑ i ∈ s, (f i).support.sup degb :=
  (sup_support_multiset_prod_le degb0 degbm _).trans_eq <| congr_arg _ <| Multiset.map_map _ _ _
Subadditivity of Sup-Degree under Finite Product in Additive Monoid Algebra
Informal description
Let $R$ be a semiring and $A$ a join-semilattice. Given a function $\operatorname{degb} \colon A \to B$ that satisfies: 1. $\operatorname{degb}(0) \leq 0$, and 2. $\operatorname{degb}(a + b) \leq \operatorname{degb}(a) + \operatorname{degb}(b)$ for all $a, b \in A$, then for any finite index set $s$ and any family of elements $(f_i)_{i \in s}$ in the additive monoid algebra $R[A]$, the supremum of $\operatorname{degb}$ over the support of the product $\prod_{i \in s} f_i$ is bounded by the sum of the suprema over the supports of the individual $f_i$: \[ \sup_{x \in \operatorname{supp}(\prod_{i \in s} f_i)} \operatorname{degb}(x) \leq \sum_{i \in s} \left( \sup_{x \in \operatorname{supp}(f_i)} \operatorname{degb}(x) \right). \]
AddMonoidAlgebra.le_inf_support_finset_prod theorem
(degt0 : 0 ≤ degt 0) (degtm : ∀ a b, degt a + degt b ≤ degt (a + b)) (s : Finset ι) (f : ι → R[A]) : (∑ i ∈ s, (f i).support.inf degt) ≤ (∏ i ∈ s, f i).support.inf degt
Full source 
theorem le_inf_support_finset_prod (degt0 : 0 ≤ degt 0)
    (degtm : ∀ a b, degt a + degt b ≤ degt (a + b)) (s : Finset ι) (f : ι → R[A]) :
    (∑ i ∈ s, (f i).support.inf degt) ≤ (∏ i ∈ s, f i).support.inf degt :=
  le_of_eq_of_le (by rw [Multiset.map_map]; rfl) (le_inf_support_multiset_prod degt0 degtm _)
Superadditivity of Inf-Degree under Finite Product in Additive Monoid Algebra
Informal description
Let $R$ be a semiring and $A$ a meet-semilattice. Given a function $\operatorname{degt} \colon A \to T$ that satisfies: 1. $0 \leq \operatorname{degt}(0)$, and 2. $\operatorname{degt}(a) + \operatorname{degt}(b) \leq \operatorname{degt}(a + b)$ for all $a, b \in A$, then for any finite index set $s$ and any family of elements $(f_i)_{i \in s}$ in the additive monoid algebra $R[A]$, the infimum of $\operatorname{degt}$ over the support of the product $\prod_{i \in s} f_i$ is bounded below by the sum of the infima over the supports of the individual $f_i$: \[ \sum_{i \in s} \left( \inf_{x \in \operatorname{supp}(f_i)} \operatorname{degt}(x) \right) \leq \inf_{x \in \operatorname{supp}(\prod_{i \in s} f_i)} \operatorname{degt}(x). \]
AddMonoidAlgebra.supDegree abbrev
(f : R[A]) : B
Full source 
/-- Let `R` be a semiring, let `A` be an `AddZeroClass`, let `B` be an `OrderBot`,
and let `D : A → B` be a "degree" function.
For an element `f : R[A]`, the element `supDegree f : B` is the supremum of all the elements in the
support of `f`, or `⊥` if `f` is zero.
Often, the Type `B` is `WithBot A`,
If, further, `A` has a linear order, then this notion coincides with the usual one,
using the maximum of the exponents.

If `A := σ →₀ ℕ` then `R[A] = MvPolynomial σ R`, and if we equip `σ` with a linear order then
the induced linear order on `Lex A` equips `MvPolynomial` ring with a
[monomial order](https://en.wikipedia.org/wiki/Monomial_order) (i.e. a linear order on `A`, the
type of (monic) monomials in `R[A]`, that respects addition). We make use of this monomial order
by taking `D := toLex`, and different monomial orders could be accessed via different type
synonyms once they are added. -/
abbrev supDegree (f : R[A]) : B :=
  f.support.sup D
Supremum Degree of an Additive Monoid Algebra Element
Informal description
Let $R$ be a semiring, $A$ an `AddZeroClass`, and $B$ an `OrderBot` with a degree function $D : A \to B$. For an element $f \in R[A]$, the *sup-degree* of $f$, denoted $\text{supDegree}(f)$, is the supremum of the degrees of all monomials appearing in the support of $f$, or $\bot$ if $f = 0$. When $B = \text{WithBot}\,A$ and $A$ is linearly ordered, this coincides with the usual notion of degree (the maximum exponent of monomials with nonzero coefficients).
AddMonoidAlgebra.supDegree_add_le theorem
{f g : R[A]} : (f + g).supDegree D ≤ (f.supDegree D) ⊔ (g.supDegree D)
Full source 
theorem supDegree_add_le {f g : R[A]} :
    (f + g).supDegree D ≤ (f.supDegree D) ⊔ (g.supDegree D) :=
  sup_support_add_le D f g
Sup-degree of sum is bounded by join of sup-degrees in additive monoid algebra
Informal description
Let $R$ be a semiring and $A$ an additive monoid. For any two elements $f, g \in R[A]$ and a degree function $D \colon A \to B$ where $B$ is an ordered type with a bottom element, the sup-degree of the sum $f + g$ satisfies the inequality: $$\text{supDegree}(f + g) \leq \text{supDegree}(f) \sqcup \text{supDegree}(g).$$
AddMonoidAlgebra.supDegree_neg theorem
{f : R'[A]} : (-f).supDegree D = f.supDegree D
Full source 
@[simp]
theorem supDegree_neg {f : R'[A]} :
    (-f).supDegree D = f.supDegree D := by
  rw [supDegree, supDegree, Finsupp.support_neg]
Sup-degree is invariant under negation in additive monoid algebras
Informal description
Let $R'$ be a ring, $A$ an additive monoid, and $D \colon A \to B$ a degree function where $B$ is an ordered type with a bottom element. For any element $f \in R'[A]$, the sup-degree of $-f$ is equal to the sup-degree of $f$, i.e., $$\text{supDegree}(-f) = \text{supDegree}(f).$$
AddMonoidAlgebra.supDegree_sub_le theorem
{f g : R'[A]} : (f - g).supDegree D ≤ f.supDegree D ⊔ g.supDegree D
Full source 
theorem supDegree_sub_le {f g : R'[A]} :
    (f - g).supDegree D ≤ f.supDegree D ⊔ g.supDegree D := by
  rw [sub_eq_add_neg, ← supDegree_neg (f := g)]; apply supDegree_add_le
Sup-degree of difference is bounded by join of sup-degrees in additive monoid algebra
Informal description
Let $R'$ be a ring and $A$ an additive monoid. For any two elements $f, g \in R'[A]$ and a degree function $D \colon A \to B$ where $B$ is an ordered type with a bottom element, the sup-degree of the difference $f - g$ satisfies the inequality: $$\text{supDegree}(f - g) \leq \text{supDegree}(f) \sqcup \text{supDegree}(g).$$
AddMonoidAlgebra.supDegree_sum_le theorem
{ι} {s : Finset ι} {f : ι → R[A]} : (∑ i ∈ s, f i).supDegree D ≤ s.sup (fun i => (f i).supDegree D)
Full source 
theorem supDegree_sum_le {ι} {s : Finset ι} {f : ι → R[A]} :
    (∑ i ∈ s, f i).supDegree D ≤ s.sup (fun i => (f i).supDegree D) := by
  classical
  exact (Finset.sup_mono Finsupp.support_finset_sum).trans_eq (Finset.sup_biUnion _ _)
Sup-degree of sum is bounded by supremum of sup-degrees in additive monoid algebra
Informal description
Let $R$ be a semiring, $A$ an additive monoid, and $B$ an ordered type with a bottom element $\bot$, equipped with a degree function $D \colon A \to B$. For any finite set $s$ of indices and any family of elements $f_i \in R[A]$ indexed by $i \in s$, the sup-degree of the sum $\sum_{i \in s} f_i$ is bounded above by the supremum of the sup-degrees of the $f_i$: \[ \text{supDegree}\left(\sum_{i \in s} f_i\right) \leq \sup_{i \in s} \text{supDegree}(f_i). \]
AddMonoidAlgebra.supDegree_single_ne_zero theorem
(a : A) {r : R} (hr : r ≠ 0) : (single a r).supDegree D = D a
Full source 
theorem supDegree_single_ne_zero (a : A) {r : R} (hr : r ≠ 0) :
    (single a r).supDegree D = D a := by
  rw [supDegree, Finsupp.support_single_ne_zero a hr, Finset.sup_singleton]
Sup-Degree of Nonzero Single Generator in Additive Monoid Algebra: $\text{supDegree}(\text{single}(a, r)) = D(a)$ for $r \neq 0$
Informal description
Let $R$ be a semiring, $A$ an `AddZeroClass`, and $B$ an `OrderBot` with a degree function $D : A \to B$. For any element $a \in A$ and any nonzero element $r \in R$, the sup-degree of the single generator $\text{single}(a, r) \in R[A]$ is equal to $D(a)$, i.e., \[ \text{supDegree}(\text{single}(a, r)) = D(a). \]
AddMonoidAlgebra.supDegree_single theorem
(a : A) (r : R) : (single a r).supDegree D = if r = 0 then ⊥ else D a
Full source 
theorem supDegree_single (a : A) (r : R) :
    (single a r).supDegree D = if r = 0 then ⊥ else D a := by
  split_ifs with hr <;> simp [supDegree_single_ne_zero, hr]
Sup-Degree of Single Generator in Additive Monoid Algebra: $\text{supDegree}(\text{single}(a, r)) = D(a)$ if $r \neq 0$, $\bot$ otherwise
Informal description
Let $R$ be a semiring, $A$ an additive monoid, and $B$ an ordered type with a bottom element $\bot$, equipped with a degree function $D : A \to B$. For any element $a \in A$ and coefficient $r \in R$, the sup-degree of the single generator $\text{single}(a, r) \in R[A]$ is given by: \[ \text{supDegree}(\text{single}(a, r)) = \begin{cases} D(a) & \text{if } r \neq 0, \\ \bot & \text{if } r = 0. \end{cases} \]
AddMonoidAlgebra.apply_eq_zero_of_not_le_supDegree theorem
{p : R[A]} {a : A} (hlt : ¬ D a ≤ p.supDegree D) : p a = 0
Full source 
theorem apply_eq_zero_of_not_le_supDegree {p : R[A]} {a : A} (hlt : ¬ D a ≤ p.supDegree D) :
    p a = 0 := by
  contrapose! hlt
  exact Finset.le_sup (Finsupp.mem_support_iff.2 hlt)
Vanishing of Coefficients Below Sup-Degree in Additive Monoid Algebra
Informal description
Let $R$ be a semiring and $A$ an additive monoid, equipped with a degree function $D \colon A \to B$ where $B$ is an ordered type with a bottom element $\bot$. For any element $p \in R[A]$ and any $a \in A$, if $D(a)$ is not less than or equal to the sup-degree of $p$ (i.e., $\neg (D(a) \leq \text{supDegree}(p))$), then the coefficient of $a$ in $p$ is zero, i.e., $p(a) = 0$.
AddMonoidAlgebra.supDegree_withBot_some_comp theorem
{s : AddMonoidAlgebra R A} (hs : s.support.Nonempty) : supDegree (WithBot.some ∘ D) s = supDegree D s
Full source 
theorem supDegree_withBot_some_comp {s : AddMonoidAlgebra R A} (hs : s.support.Nonempty) :
    supDegree (WithBot.someWithBot.some ∘ D) s = supDegree D s := by
  unfold AddMonoidAlgebra.supDegree
  rw [← Finset.coe_sup' hs, Finset.sup'_eq_sup]
Equality of Sup-Degrees under Composition with $\text{WithBot.some}$ for Nonzero Elements
Informal description
Let $R$ be a semiring and $A$ an additive monoid, with a degree function $D \colon A \to B$ where $B$ is an ordered type with a bottom element $\bot$. For any nonzero element $s \in R[A]$ (i.e., with nonempty support), the sup-degree of $s$ with respect to the composition $\text{WithBot.some} \circ D$ is equal to the sup-degree of $s$ with respect to $D$. In other words, if $s \neq 0$, then: \[ \text{supDegree}(\text{WithBot.some} \circ D)(s) = \text{supDegree}(D)(s). \]
AddMonoidAlgebra.supDegree_eq_of_isMaxOn theorem
{p : R[A]} {a : A} (hmem : a ∈ p.support) (hmax : IsMaxOn D p.support a) : p.supDegree D = D a
Full source 
theorem supDegree_eq_of_isMaxOn {p : R[A]} {a : A} (hmem : a ∈ p.support)
    (hmax : IsMaxOn D p.support a) : p.supDegree D = D a :=
  sup_eq_of_isMaxOn hmem hmax
Sup-Degree Equals Degree at Maximum Point in Additive Monoid Algebra
Informal description
Let $R$ be a semiring and $A$ a join-semilattice. Given an element $p \in R[A]$ and a point $a$ in the support of $p$ (i.e., $a \in \text{supp}(p)$), if $a$ maximizes the degree function $D$ on $\text{supp}(p)$ (i.e., $D(x) \leq D(a)$ for all $x \in \text{supp}(p)$), then the sup-degree of $p$ equals $D(a)$, i.e., $\text{supDegree}_D(p) = D(a)$.
AddMonoidAlgebra.infDegree abbrev
(f : R[A]) : T
Full source 
/-- Let `R` be a semiring, let `A` be an `AddZeroClass`, let `T` be an `OrderTop`,
and let `D : A → T` be a "degree" function.
For an element `f : R[A]`, the element `infDegree f : T` is the infimum of all the elements in the
support of `f`, or `⊤` if `f` is zero.
Often, the Type `T` is `WithTop A`,
If, further, `A` has a linear order, then this notion coincides with the usual one,
using the minimum of the exponents. -/
abbrev infDegree (f : R[A]) : T :=
  f.support.inf D
Infimum degree of an additive monoid algebra element
Informal description
Let $R$ be a semiring, $A$ be an additive monoid, $T$ be an ordered type with a top element $\top$, and $D \colon A \to T$ be a degree function. For an element $f \in R[A]$, the *inf-degree* of $f$, denoted $\inf\!\text{-degree}_D(f) \in T$, is defined as the infimum of $D(a)$ over all $a$ in the support of $f$ (i.e., where $f(a) \neq 0$), or $\top$ if $f = 0$. When $T = \text{WithTop}\,A$ and $A$ is linearly ordered, this coincides with the minimum exponent appearing in $f$ (or $\top$ if $f = 0$).
AddMonoidAlgebra.le_infDegree_add theorem
(f g : R[A]) : (f.infDegree D) ⊓ (g.infDegree D) ≤ (f + g).infDegree D
Full source 
theorem le_infDegree_add (f g : R[A]) :
    (f.infDegree D) ⊓ (g.infDegree D) ≤ (f + g).infDegree D :=
  le_inf_support_add D f g
Inf-Degree Subadditivity in Additive Monoid Algebra
Informal description
Let $R$ be a semiring and $A$ an additive monoid. For any two elements $f, g \in R[A]$, the infimum of their inf-degrees with respect to a degree function $D$ is less than or equal to the inf-degree of their sum: $$\inf\!\text{-degree}_D(f) \sqcap \inf\!\text{-degree}_D(g) \leq \inf\!\text{-degree}_D(f + g).$$ Here, $\inf\!\text{-degree}_D(f)$ denotes the infimum of $D(a)$ over all $a$ in the support of $f$ (or $\top$ if $f = 0$), and $\sqcap$ is the meet operation in the codomain of $D$.
AddMonoidAlgebra.infDegree_withTop_some_comp theorem
{s : AddMonoidAlgebra R A} (hs : s.support.Nonempty) : infDegree (WithTop.some ∘ D) s = infDegree D s
Full source 
theorem infDegree_withTop_some_comp {s : AddMonoidAlgebra R A} (hs : s.support.Nonempty) :
    infDegree (WithTop.someWithTop.some ∘ D) s = infDegree D s := by
  unfold AddMonoidAlgebra.infDegree
  rw [← Finset.coe_inf' hs, Finset.inf'_eq_inf]
Equality of Inf-Degrees under Composition with $\text{WithTop.some}$
Informal description
Let $R$ be a semiring and $A$ an additive monoid. For a non-zero element $s \in R[A]$ (i.e., the support of $s$ is nonempty) and a degree function $D \colon A \to \alpha$, the inf-degree of $s$ with respect to the composition $\text{WithTop.some} \circ D$ is equal to the inf-degree of $s$ with respect to $D$. In other words, $$\inf\!\text{-degree}_{\text{WithTop.some} \circ D}(s) = \inf\!\text{-degree}_D(s).$$
AddMonoidAlgebra.le_infDegree_mul theorem
[AddZeroClass A] [Add T] [AddLeftMono T] [AddRightMono T] (D : AddHom A T) (f g : R[A]) : f.infDegree D + g.infDegree D ≤ (f * g).infDegree D
Full source 
theorem le_infDegree_mul [AddZeroClass A] [Add T] [AddLeftMono T] [AddRightMono T]
    (D : AddHom A T) (f g : R[A]) :
    f.infDegree D + g.infDegree D ≤ (f * g).infDegree D :=
  le_inf_support_mul (fun {a b : A} => (map_add D a b).ge) _ _
Subadditivity of Inf-Degree under Multiplication in Additive Monoid Algebra
Informal description
Let $R$ be a semiring, $A$ an additive monoid with a zero element, and $T$ an additive monoid where addition is left and right monotone. Given an additive homomorphism $D \colon A \to T$ and two elements $f, g \in R[A]$, the sum of their inf-degrees with respect to $D$ is less than or equal to the inf-degree of their product: \[ \inf\!\text{-degree}_D(f) + \inf\!\text{-degree}_D(g) \leq \inf\!\text{-degree}_D(f * g). \] Here, $\inf\!\text{-degree}_D(f)$ denotes the infimum of $D(a)$ over all $a$ in the support of $f$ (or the top element of $T$ if $f = 0$), and $f * g$ is the convolution product in $R[A]$.