English
If a polynomial f on a finite set of variables has total degree less than n times the number of variables, then every exponent vector occurring in f has some component less than n.
Русский
Если полином f в конечном числе переменных имеет общую степень, меньшую чем n умножить на число переменных, тогда в каждом представлении f встречается хотя бы один показатель степени, не достигающий n.
LaTeX
$$$\\\\forall f : MvPolynomial σ R,\\\\forall n : \\mathbb{N},\\\\ f.totalDegree < n * |σ| \\\\Rightarrow \\\\forall d \\\\in f.support, \\\\exists i \\\\in σ, \\\\ d i < n$$$
Lean4
theorem exists_degree_lt [Fintype σ] (f : MvPolynomial σ R) (n : ℕ) (h : f.totalDegree < n * Fintype.card σ)
{d : σ →₀ ℕ} (hd : d ∈ f.support) : ∃ i, d i < n :=
by
contrapose! h
calc
n * Fintype.card σ = ∑ _s : σ, n := by rw [Finset.sum_const, Nat.nsmul_eq_mul, mul_comm, Finset.card_univ]
_ ≤ ∑ s, d s := (Finset.sum_le_sum fun s _ => h s)
_ ≤ d.sum fun _ e => e := by
rw [Finsupp.sum_fintype]
intros
rfl
_ ≤ f.totalDegree := le_totalDegree hd
