English
A multiplication induction lemma: under suitable degree and support bounds, reflect (N+O) (f g) equals reflect N f times reflect O g.
Русский
Лемма индукции умножения: при надлежащих ограничениях по степеням и поддержке выполняется reflect(N+O)(f g) = reflect N f · reflect O g.
LaTeX
$$$\\text{reflect}(N+O)(f g) = \\text{reflect}(N) f \\cdot \\text{reflect}(O) g$ under the specified bounds on supports and degrees.$$
Lean4
theorem reflect_mul_induction (cf cg : ℕ) (N O : ℕ) (f g : R[X]) (Cf : #f.support ≤ cf.succ) (Cg : #g.support ≤ cg.succ)
(Nf : f.natDegree ≤ N) (Og : g.natDegree ≤ O) : reflect (N + O) (f * g) = reflect N f * reflect O g := by
induction cf generalizing f with
| zero =>
induction cg generalizing g with
| zero =>
rw [← C_mul_X_pow_eq_self Cf, ← C_mul_X_pow_eq_self Cg]
simp_rw [mul_assoc, X_pow_mul, mul_assoc, ← pow_add (X : R[X]), reflect_C_mul, reflect_monomial, add_comm,
revAt_add Nf Og, mul_assoc, X_pow_mul, mul_assoc, ← pow_add (X : R[X]), add_comm]
| succ cg hcg =>
by_cases g0 : g = 0
· rw [g0, reflect_zero, mul_zero, mul_zero, reflect_zero]
rw [← eraseLead_add_C_mul_X_pow g, mul_add, reflect_add, reflect_add, mul_add, hcg, hcg] <;> try assumption
· exact le_add_left card_support_C_mul_X_pow_le_one
· exact le_trans (natDegree_C_mul_X_pow_le g.leadingCoeff g.natDegree) Og
· exact Nat.lt_succ_iff.mp (lt_of_lt_of_le (eraseLead_support_card_lt g0) Cg)
· exact le_trans eraseLead_natDegree_le_aux Og
| succ cf hcf =>
by_cases f0 : f = 0
· rw [f0, reflect_zero, zero_mul, zero_mul, reflect_zero]
rw [← eraseLead_add_C_mul_X_pow f, add_mul, reflect_add, reflect_add, add_mul, hcf, hcf] <;> try assumption
· exact le_add_left card_support_C_mul_X_pow_le_one
· exact le_trans (natDegree_C_mul_X_pow_le f.leadingCoeff f.natDegree) Nf
· exact Nat.lt_succ_iff.mp (lt_of_lt_of_le (eraseLead_support_card_lt f0) Cf)
· exact le_trans eraseLead_natDegree_le_aux Nf
