English
Let P be a predicate on polynomials. If P holds for the zero polynomial, P holds for every monomial C r X^n with n ≤ N and r ≠ 0, and P is closed under addition of polynomials whose leading natDegree terms grow strictly (i.e., if f.natDegree < g.natDegree and g.natDegree ≤ N, then P(f) and P(g) imply P(f+g)), then P holds for every polynomial f with natDegree ≤ N.
Русский
Пусть P — предикат на многочленах. Если P верно для нулевого многочлена, P верно для каждого монома C r X^n с n ≤ N и r ≠ 0, и P сохраняется при сложении полиномов, если высшая степень natDegree увеличивается строго (то есть если f.natDegree < g.natDegree и g.natDegree ≤ N, то P(f) и P(g) следуют P(f+g)), тогда P верно для любого многочлена f с natDegree ≤ N.
LaTeX
$$$\\text{Let } P: (R[X] \\to \\mathrm{Prop}) \\text{ be a predicate on polynomials. For a fixed } N \\in \\mathbb{N},\\quad P(0) \\\\land \\\\bigl(\\forall n, \\forall r\\,(r \\neq 0)\\,\\land\, n \\le N \\Rightarrow P(C\\,r\\,X^n)\\bigr) \\\\land \\\\bigl(\\forall f,g \\in R[X],\\ f.natDegree < g.natDegree \\Rightarrow g.natDegree \\le N \\Rightarrow P(f) \\Rightarrow P(g) \\Rightarrow P(f+g)\\bigr) \\\\Rightarrow \\forall f \\in R[X], f.natDegree \\le N \\Rightarrow P(f).$$$
Lean4
/-- An induction lemma for polynomials. It takes a natural number `N` as a parameter, that is
required to be at least as big as the `natDegree` of the polynomial. This is useful to prove
results where you want to change each term in a polynomial to something else depending on the
`natDegree` of the polynomial itself and not on the specific `natDegree` of each term. -/
theorem induction_with_natDegree_le (motive : R[X] → Prop) (N : ℕ) (zero : motive 0)
(C_mul_pow : ∀ n : ℕ, ∀ r : R, r ≠ 0 → n ≤ N → motive (C r * X ^ n))
(add : ∀ f g : R[X], f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)) (f : R[X])
(df : f.natDegree ≤ N) : motive f := by
induction hf : #f.support generalizing f with
| zero =>
convert zero
simpa [support_eq_empty, card_eq_zero] using hf
| succ c hc =>
rw [← eraseLead_add_C_mul_X_pow f]
cases c
· convert C_mul_pow f.natDegree f.leadingCoeff ?_ df using 1
· convert zero_add (C (leadingCoeff f) * X ^ f.natDegree)
rw [← card_support_eq_zero, card_support_eraseLead' hf]
· rw [leadingCoeff_ne_zero, Ne, ← card_support_eq_zero, hf]
exact zero_ne_one.symm
refine add f.eraseLead _ ?_ ?_ ?_ ?_
· refine (eraseLead_natDegree_lt ?_).trans_le (le_of_eq ?_)
· exact (Nat.succ_le_succ (Nat.succ_le_succ (Nat.zero_le _))).trans hf.ge
· rw [natDegree_C_mul_X_pow _ _ (leadingCoeff_ne_zero.mpr _)]
rintro rfl
simp at hf
· exact (natDegree_C_mul_X_pow_le f.leadingCoeff f.natDegree).trans df
· exact hc _ (eraseLead_natDegree_le_aux.trans df) (card_support_eraseLead' hf)
· refine C_mul_pow _ _ ?_ df
rw [Ne, leadingCoeff_eq_zero, ← card_support_eq_zero, hf]
exact Nat.succ_ne_zero _
