English
For p ∈ R[X], q ∈ Nat, with hk: q ≤ k, there exists gp ∈ R[X] with natDegree ≤ natDegree(p) − k and ∀ r ∈ A, aeval r (derivative^[k] p) = q! · aeval r gp.
Русский
Для p ∈ R[X], q ∈ Nat и hk: q ≤ k существует gp ∈ R[X] с ограничением по степеням и для всех r ∈ A выполняется aeval r(derivative^[k] p) = q! · aeval r gp.
LaTeX
$$$$ \exists gp ∈ R[X], \; \operatorname{natDegree}(gp) ≤ \operatorname{natDegree}(p) - k \; \wedge\; \forall r \in A, \ \mathrm{aeval}_r(\partial^k p) = q! \cdot \mathrm{aeval}_r gp. $$$$
Lean4
theorem aeval_iterate_derivative_of_ge (p : R[X]) (q : ℕ) {k : ℕ} (hk : q ≤ k) :
∃ gp : R[X], gp.natDegree ≤ p.natDegree - k ∧ ∀ r : A, aeval r (derivative^[k] p) = q ! • aeval r gp :=
by
obtain ⟨p', p'_le, hp'⟩ := exists_iterate_derivative_eq_factorial_smul p k
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hk
refine ⟨((q + k).descFactorial k : R[X]) * p', (natDegree_C_mul_le _ _).trans p'_le, fun r => ?_⟩
simp_rw [hp', nsmul_eq_mul, map_mul, map_natCast, ← mul_assoc, ← Nat.cast_mul, Nat.add_descFactorial_eq_ascFactorial,
Nat.factorial_mul_ascFactorial]
