English
There exists gp ∈ R[X] such that gp.natDegree ≤ p.natDegree − q and ∀ r ∈ A, for all divisibility conditions (X − C r)^q ∣ p.map(algebraMap R A) implies aeval r (sumIDeriv p) = q! · aeval r gp.
Русский
Существует gp ∈ R[X], такое что gp.natDegree ≤ p.natDegree − q и ∀ r ∈ A при условии делимости (X − C r)^q делит p.map(algebraMap R A), выполняется aeval r (sumIDeriv p) = q! · aeval r gp.
LaTeX
$$$$ \exists gp ∈ R[X], \; \operatorname{natDegree}(gp) ≤ \operatorname{natDegree}(p) - q \; \wedge\; \forall r ∈ A,\;(X - C r)^q \mid p.map(algebraMap R A) \Rightarrow \mathrm{aeval}_r(\mathrm{sumIDeriv} p) = q! \cdot \mathrm{aeval}_r gp. $$$$
Lean4
theorem aeval_sumIDeriv (p : R[X]) (q : ℕ) :
∃ gp : R[X],
gp.natDegree ≤ p.natDegree - q ∧
∀ (r : A), (X - C r) ^ q ∣ p.map (algebraMap R A) → aeval r (sumIDeriv p) = q ! • aeval r gp :=
by
have h (k) :
∃ gp : R[X],
gp.natDegree ≤ p.natDegree - q ∧
∀ (r : A), (X - C r) ^ q ∣ p.map (algebraMap R A) → aeval r (derivative^[k] p) = q ! • aeval r gp :=
by
cases lt_or_ge k q with
| inl hk =>
use 0
rw [natDegree_zero]
use Nat.zero_le _
intro r ⟨p', hp⟩
rw [map_zero, smul_zero, aeval_iterate_derivative_of_lt p q r hp hk]
| inr hk =>
obtain ⟨gp, gp_le, h⟩ := aeval_iterate_derivative_of_ge A p q hk
exact ⟨gp, gp_le.trans (tsub_le_tsub_left hk _), fun r _ => h r⟩
choose c h using h
choose c_le hc using h
refine ⟨(range (p.natDegree + 1)).sum c, ?_, ?_⟩
· refine (natDegree_sum_le _ _).trans ?_
rw [fold_max_le]
exact ⟨Nat.zero_le _, fun i _ => c_le i⟩
intro r ⟨p', hp⟩
rw [sumIDeriv_apply, map_sum]; simp_rw [hc _ r ⟨_, hp⟩, map_sum, smul_sum]
