English
For f ∈ MvPolynomial(Fin(n+1)) and i, if (finSuccEquiv R n f).coeff i ≠ 0, then the total degree bound holds as in the prior totalDegree statement.
Русский
Для f ∈ MvPolynomial(Fin(n+1)) и i, если (finSuccEquiv R n f).coeff i ≠ 0, то выполняется ограничение по общей степени как ранее.
LaTeX
$$$\\text{If } (\\operatorname{finSuccEquiv} \\; R \\; n \\; f).\\coeff i \\neq 0, \\quad \\operatorname{totalDegree}(((\\operatorname{finSuccEquiv} R n f).\\coeff i)) + i \\le \\operatorname{totalDegree} f$$$
Lean4
/-- The `totalDegree` of a multivariable polynomial `p` is at least `i` more than the `totalDegree` of
the `i`th coefficient of `finSuccEquiv` applied to `p`, if this is nonzero.
-/
theorem totalDegree_coeff_finSuccEquiv_add_le (f : MvPolynomial (Fin (n + 1)) R) (i : ℕ)
(hi : (finSuccEquiv R n f).coeff i ≠ 0) : totalDegree ((finSuccEquiv R n f).coeff i) + i ≤ totalDegree f :=
by
have hf'_sup : ((finSuccEquiv R n f).coeff i).support.Nonempty :=
by
rw [Finset.nonempty_iff_ne_empty, ne_eq, support_eq_empty]
exact hi
have ⟨σ, hσ1, hσ2⟩ :=
Finset.exists_mem_eq_sup (support _) hf'_sup
(fun s => Finsupp.sum s fun _ e => e)
-- Then cons i σ is a monomial index of p with total degree equal to the desired bound
let σ' : Fin (n + 1) →₀ ℕ := cons i σ
convert le_totalDegree (s := σ') _
· rw [totalDegree, hσ2, sum_cons, add_comm]
· rw [← support_coeff_finSuccEquiv]
exact hσ1
