AddMonoidAlgebra.sup_support_list_prod_le
theorem AddMonoidAlgebra.sup_support_list_prod_le :
∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : SemilatticeSup B] [inst_1 : OrderBot B] [inst_2 : Semiring R]
[inst_3 : AddMonoid A] [inst_4 : AddMonoid B]
[inst_5 : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst_6 : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {degb : A → B},
degb 0 ≤ 0 →
(∀ (a b : A), degb (a + b) ≤ degb a + degb b) →
∀ (l : List (AddMonoidAlgebra R A)),
l.prod.support.sup degb ≤ (List.map (fun f => f.support.sup degb) l).sum
This theorem states that for any semiring `R`, additive monoids `A` and `B`, and a function `degb` from `A` to `B`, if `degb` maps the zero element of `A` to a value less than or equal to zero and for all elements `a` and `b` of `A`, `degb` of their sum is less than or equal to the sum of `degb` of `a` and `degb` of `b`, then for any list of elements of the add monoid algebra of `R` and `A`, the supremum of the support of the product of the list elements under `degb` is less than or equal to the sum of the supremum of the support of each element under `degb`. This is a property related to the order and operations in the set-up monoids and semiring, particularly regarding convolutions in the monoid algebra and operations on finite sets.
More concisely: For any semiring `R`, additive monoids `A` and `B`, and a degree function `degb` from `A` to `B` with `degb(0) ≤ 0` and `degb(a + b) ≤ degb(a) + degb(b)` for all `a, b` in `A`, the supremum of `degb` over the support of a product of elements in the monoid algebra of `R` and `A` is less than or equal to the sum of the supremum of `degb` over the support of each element.
|
AddMonoidAlgebra.sup_support_add_le
theorem AddMonoidAlgebra.sup_support_add_le :
∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : SemilatticeSup B] [inst_1 : OrderBot B] [inst_2 : Semiring R]
(degb : A → B) (f g : AddMonoidAlgebra R A), (f + g).support.sup degb ≤ f.support.sup degb ⊔ g.support.sup degb
The theorem `AddMonoidAlgebra.sup_support_add_le` states that for any semiring `R`, types `A` and `B`, a function `degb : A → B`, and two elements `f` and `g` of the add monoid algebra generated by `A` over `R`, the supremum (greatest element) of the set `{degb x | x ∈ support(f + g)}` is less than or equal to the supremum of the set `{degb x | x ∈ support(f)}` joined with the supremum of the set `{degb x | x ∈ support(g)}`. Here, `support(f)` denotes the set of elements in `A` that appear in the formal combination `f` with a non-zero coefficient. The join operation `⊔` is defined on `B` which is assumed to be a semilattice with a bottom element.
More concisely: For any semiring R, types A and B, a function degb : A → B, and elements f and g of the add monoid algebra over R generated by A, the supremum of degb over the support of f + g is less than or equal to the join of the supremum of degb over the support of f and the supremum of degb over the support of g.
|
AddMonoidAlgebra.sup_support_mul_le
theorem AddMonoidAlgebra.sup_support_mul_le :
∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : SemilatticeSup B] [inst_1 : OrderBot B] [inst_2 : Semiring R]
[inst_3 : Add A] [inst_4 : Add B] [inst_5 : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst_6 : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {degb : A → B},
(∀ {a b : A}, degb (a + b) ≤ degb a + degb b) →
∀ (f g : AddMonoidAlgebra R A), (f * g).support.sup degb ≤ f.support.sup degb + g.support.sup degb
The theorem `AddMonoidAlgebra.sup_support_mul_le` states that for any types `R`, `A`, and `B` where `A` is an additive monoid, `B` is a semilattice with a bottom element, and `R` is a semiring, if you have a function `degb` from `A` to `B` that satisfies the property that for any two elements `a` and `b` of `A`, `degb` of their sum is less than or equal to the sum of their `degb` values, then for any two elements `f` and `g` of the monoid algebra of `A` over `R`, the supremum of the `degb` values over the support of the product of `f` and `g` is less than or equal to the sum of the suprema of the `degb` values over the supports of `f` and `g`. This theorem is a statement about the behavior of a specific type of algebraic structure (the monoid algebra) under a specific type of operation (the supremum over a function of the support of an element).
More concisely: Given an additive monoid `A`, a semilattice with a bottom element `B`, and a semiring `R`, if `degb` is a function from `A` to `B` satisfying `degb(a + b) <= degb(a) + degb(b)` for all `a, b` in `A`, then for any `f, g` in the monoid algebra of `A` over `R`, `sup (degb . support f) + sup (degb . support g) >= sup (degb . support (f * g))`. (Note: The inequality in the theorem is reversed due to the different conventions in Lean and mathematical notation for supremum.)
|