English
For polynomials p,q over a ring, natDegree(p ∘ q) ≤ natDegree(p) · natDegree(q).
Русский
Для многочленов p,q над кольцом верно, что natDegree(p ∘ q) ≤ natDegree(p) · natDegree(q).
LaTeX
$$$\\operatorname{natDegree}\\bigl(p \\circ q\\bigr) \\le \\operatorname{natDegree}(p) \\cdot \\operatorname{natDegree}(q)$$$
Lean4
theorem natDegree_comp_le : natDegree (p.comp q) ≤ natDegree p * natDegree q :=
letI := Classical.decEq R
if h0 : p.comp q = 0 then by rw [h0, natDegree_zero]; exact Nat.zero_le _
else
WithBot.coe_le_coe.1 <|
calc
↑(natDegree (p.comp q)) = degree (p.comp q) := (degree_eq_natDegree h0).symm
_ = _ := (congr_arg degree comp_eq_sum_left)
_ ≤ _ := (degree_sum_le _ _)
_ ≤ _ :=
Finset.sup_le fun n hn =>
calc
degree (C (coeff p n) * q ^ n) ≤ degree (C (coeff p n)) + degree (q ^ n) := degree_mul_le _ _
_ ≤ natDegree (C (coeff p n)) + n • degree q := (add_le_add degree_le_natDegree (degree_pow_le _ _))
_ ≤ natDegree (C (coeff p n)) + n • ↑(natDegree q) :=
(add_le_add_left (nsmul_le_nsmul_right (@degree_le_natDegree _ _ q) n) _)
_ = (n * natDegree q : ℕ) :=
by
rw [natDegree_C, Nat.cast_zero, zero_add, nsmul_eq_mul]
simp
_ ≤ (natDegree p * natDegree q : ℕ) :=
WithBot.coe_le_coe.2 <|
mul_le_mul_of_nonneg_right (le_natDegree_of_ne_zero (mem_support_iff.1 hn)) (Nat.zero_le _)
