English
Given a multivariate polynomial F with total degree at most m, and polynomials f_i with natDegree at most n for each index i, the natDegree of the evaluated polynomial aeval_f(F) is at most m n.
Русский
Пусть F — многочлен с суммарной степенью не более m, а для каждого индекса i полином f_i имеет натуральную степень не более n. Тогда natDegree( aeval_f(F) ) ≤ m n.
LaTeX
$$$\operatorname{natDegree}(\mathrm{aeval}_f F) \le m \cdot n$$$
Lean4
theorem aeval_natDegree_le {R : Type*} [CommSemiring R] {m n : ℕ} (F : MvPolynomial σ R) (hF : F.totalDegree ≤ m)
(f : σ → Polynomial R) (hf : ∀ i, (f i).natDegree ≤ n) : (MvPolynomial.aeval f F).natDegree ≤ m * n :=
by
rw [MvPolynomial.aeval_def, MvPolynomial.eval₂]
apply (Polynomial.natDegree_sum_le _ _).trans
apply Finset.sup_le
intro d hd
simp_rw [Function.comp_apply, ← C_eq_algebraMap]
apply (Polynomial.natDegree_C_mul_le _ _).trans
apply (Polynomial.natDegree_prod_le _ _).trans
have : ∑ i ∈ d.support, (d i) * n ≤ m * n := by
rw [← Finset.sum_mul]
apply mul_le_mul' (.trans _ hF) le_rfl
rw [MvPolynomial.totalDegree]
exact Finset.le_sup_of_le hd le_rfl
apply (Finset.sum_le_sum _).trans this
rintro i -
apply Polynomial.natDegree_pow_le.trans
exact mul_le_mul' le_rfl (hf i)
