English
For a list of elements in the monoid algebra, the supremum of the degree of the product is bounded by the sum of the supremums of the degrees of the factors.
Русский
Для списка элементов в алгебре моноидов верхняя грань степени произведения ограничена суммой верхних граней степеней множителей.
LaTeX
$$$ (l_{1}\\cdot l_{2}\\cdot\\dots)\\!\\sup \\deg ≤ \\sum (f_i)\\!\\sup \\deg$$$
Lean4
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) _)
