degree_sum_le — Mathlib

English

For any finite set s and family f, the degree of the sum over s is bounded by the supremum of the degrees: deg(sum_{x∈s} f(x)) ≤ sup_{x∈s} deg(f(x)).

Русский

Для конечного множества s и семейства функций степень суммы по s не превосходит наибольшую степень: deg(∑_{x∈s} f(x)) ≤ sup_{x∈s} deg(f(x)).

LaTeX

$$$\deg_m\Bigl(\sum_{x\in s} f(x)\Bigr) \preceq_m \sup_{x\in s} \deg_m (f(x))$$$

Lean4

theorem degree_sum_le {α : Type*} {s : Finset α} {f : α → MvPolynomial σ R} :
    (m.toSyn <| m.degree <| ∑ x ∈ s, f x) ≤ s.sup fun x ↦ (m.toSyn <| m.degree <| f x) := by
  induction s using Finset.cons_induction_on with
  | empty => simp
  | cons a s haA h =>
    rw [Finset.sum_cons, Finset.sup_cons]
    exact le_trans m.degree_add_le (max_le_max le_rfl h)

Похожие утверждения