Lemmas about the sup and inf of the support of add_monoid_algebra #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.
Results about the finset.sup and finset.inf of finsupp.support #
In this section, we use degb and degt to denote "degree functions" on A with values in
a type with bot or top respectively.
theorem
add_monoid_algebra.sup_support_mul_le
{R : Type u_1}
{A : Type u_2}
{B : Type u_4}
[semilattice_sup B]
[order_bot B]
[semiring R]
[has_add A]
[has_add B]
[covariant_class B B has_add.add has_le.le]
[covariant_class B B (function.swap has_add.add) has_le.le]
{degb : A → B}
(degbm : ∀ {a b : A}, degb (a + b) ≤ degb a + degb b)
(f g : add_monoid_algebra R A) :
theorem
add_monoid_algebra.le_inf_support_mul
{R : Type u_1}
{A : Type u_2}
{T : Type u_3}
[semilattice_inf T]
[order_top T]
[semiring R]
[has_add A]
[has_add T]
[covariant_class T T has_add.add has_le.le]
[covariant_class T T (function.swap has_add.add) has_le.le]
{degt : A → T}
(degtm : ∀ {a b : A}, degt a + degt b ≤ degt (a + b))
(f g : add_monoid_algebra R A) :
theorem
add_monoid_algebra.sup_support_list_prod_le
{R : Type u_1}
{A : Type u_2}
{B : Type u_4}
[semilattice_sup B]
[order_bot B]
[semiring R]
[add_monoid A]
[add_monoid B]
[covariant_class B B has_add.add has_le.le]
[covariant_class B B (function.swap has_add.add) has_le.le]
{degb : A → B}
(degb0 : degb 0 ≤ 0)
(degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b)
(l : list (add_monoid_algebra R A)) :
theorem
add_monoid_algebra.le_inf_support_list_prod
{R : Type u_1}
{A : Type u_2}
{T : Type u_3}
[semilattice_inf T]
[order_top T]
[semiring R]
[add_monoid A]
[add_monoid T]
[covariant_class T T has_add.add has_le.le]
[covariant_class T T (function.swap has_add.add) has_le.le]
{degt : A → T}
(degt0 : 0 ≤ degt 0)
(degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b))
(l : list (add_monoid_algebra R A)) :
theorem
add_monoid_algebra.sup_support_pow_le
{R : Type u_1}
{A : Type u_2}
{B : Type u_4}
[semilattice_sup B]
[order_bot B]
[semiring R]
[add_monoid A]
[add_monoid B]
[covariant_class B B has_add.add has_le.le]
[covariant_class B B (function.swap has_add.add) has_le.le]
{degb : A → B}
(degb0 : degb 0 ≤ 0)
(degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b)
(n : ℕ)
(f : add_monoid_algebra R A) :
theorem
add_monoid_algebra.le_inf_support_pow
{R : Type u_1}
{A : Type u_2}
{T : Type u_3}
[semilattice_inf T]
[order_top T]
[semiring R]
[add_monoid A]
[add_monoid T]
[covariant_class T T has_add.add has_le.le]
[covariant_class T T (function.swap has_add.add) has_le.le]
{degt : A → T}
(degt0 : 0 ≤ degt 0)
(degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b))
(n : ℕ)
(f : add_monoid_algebra R A) :
theorem
add_monoid_algebra.sup_support_multiset_prod_le
{R : Type u_1}
{A : Type u_2}
{B : Type u_4}
[semilattice_sup B]
[order_bot B]
[comm_semiring R]
[add_comm_monoid A]
[add_comm_monoid B]
[covariant_class B B has_add.add has_le.le]
[covariant_class B B (function.swap has_add.add) has_le.le]
{degb : A → B}
(degb0 : degb 0 ≤ 0)
(degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b)
(m : multiset (add_monoid_algebra R A)) :
m.prod.support.sup degb ≤ (multiset.map (λ (f : add_monoid_algebra R A), f.support.sup degb) m).sum
theorem
add_monoid_algebra.le_inf_support_multiset_prod
{R : Type u_1}
{A : Type u_2}
{T : Type u_3}
[semilattice_inf T]
[order_top T]
[comm_semiring R]
[add_comm_monoid A]
[add_comm_monoid T]
[covariant_class T T has_add.add has_le.le]
[covariant_class T T (function.swap has_add.add) has_le.le]
{degt : A → T}
(degt0 : 0 ≤ degt 0)
(degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b))
(m : multiset (add_monoid_algebra R A)) :
(multiset.map (λ (f : add_monoid_algebra R A), f.support.inf degt) m).sum ≤ m.prod.support.inf degt
theorem
add_monoid_algebra.sup_support_finset_prod_le
{R : Type u_1}
{A : Type u_2}
{B : Type u_4}
{ι : Type u_5}
[semilattice_sup B]
[order_bot B]
[comm_semiring R]
[add_comm_monoid A]
[add_comm_monoid B]
[covariant_class B B has_add.add has_le.le]
[covariant_class B B (function.swap has_add.add) has_le.le]
{degb : A → B}
(degb0 : degb 0 ≤ 0)
(degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b)
(s : finset ι)
(f : ι → add_monoid_algebra R A) :
theorem
add_monoid_algebra.le_inf_support_finset_prod
{R : Type u_1}
{A : Type u_2}
{T : Type u_3}
{ι : Type u_5}
[semilattice_inf T]
[order_top T]
[comm_semiring R]
[add_comm_monoid A]
[add_comm_monoid T]
[covariant_class T T has_add.add has_le.le]
[covariant_class T T (function.swap has_add.add) has_le.le]
{degt : A → T}
(degt0 : 0 ≤ degt 0)
(degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b))
(s : finset ι)
(f : ι → add_monoid_algebra R A) :