Sum of iterated derivatives

This file introduces Polynomial.sumIDeriv, the sum of the iterated derivatives of a polynomial, as a linear map. This is used in particular in the proof of the Lindemann-Weierstrass theorem (see #6718).

Main results

• Polynomial.sumIDeriv: Sum of iterated derivatives of a polynomial, as a linear map
• Polynomial.sumIDeriv_apply, Polynomial.sumIDeriv_apply_of_lt, Polynomial.sumIDeriv_apply_of_le: Polynomial.sumIDeriv expressed as a sum
• Polynomial.sumIDeriv_C, Polynomial.sumIDeriv_X: Polynomial.sumIDeriv applied to simple polynomials
• Polynomial.sumIDeriv_map: Polynomial.sumIDeriv commutes with Polynomial.map
• Polynomial.sumIDeriv_derivative: Polynomial.sumIDeriv commutes with Polynomial.derivative
• Polynomial.sumIDeriv_eq_self_add: sumIDeriv p = p + sumIDeriv (derivative p)
• Polynomial.exists_iterate_derivative_eq_factorial_smul: the k'th iterated derivative of a polynomial has a common factor k!
• Polynomial.aeval_iterate_derivative_of_lt, Polynomial.aeval_iterate_derivative_self, Polynomial.aeval_iterate_derivative_of_ge: applying Polynomial.aeval to iterated derivatives
• Polynomial.aeval_sumIDeriv, Polynomial.aeval_sumIDeriv_of_pos: applying Polynomial.aeval to Polynomial.sumIDeriv

noncomputable def Polynomial.sumIDeriv {R : Type u_1} [Semiring R] : Polynomial R →ₗ[R] Polynomial R

Sum of iterated derivatives of a polynomial, as a linear map

This definition does not allow different weights for the derivatives. It is likely that it could be extended to allow them, but this was not needed for the initial use case (the integration by part of the integral $I_i$ in the Lindemann-Weierstrass theorem).

Equations

• Polynomial.sumIDeriv = ((Finsupp.lsum ℕ) fun (x : ℕ) => LinearMap.id) ∘ₗ Polynomial.derivativeFinsupp

theorem Polynomial.sumIDeriv_apply {R : Type u_1} [Semiring R] (p : Polynomial R) : Polynomial.sumIDeriv p = ∑ i ∈ Finset.range (p.natDegree + 1), (⇑Polynomial.derivative)^[i] p

theorem Polynomial.sumIDeriv_apply_of_lt {R : Type u_1} [Semiring R] {p : Polynomial R} {n : ℕ} (hn : p.natDegree < n) : Polynomial.sumIDeriv p = ∑ i ∈ Finset.range n, (⇑Polynomial.derivative)^[i] p

theorem Polynomial.sumIDeriv_apply_of_le {R : Type u_1} [Semiring R] {p : Polynomial R} {n : ℕ} (hn : p.natDegree ≤ n) : Polynomial.sumIDeriv p = ∑ i ∈ Finset.range (n + 1), (⇑Polynomial.derivative)^[i] p

@[simp]

theorem Polynomial.sumIDeriv_C {R : Type u_1} [Semiring R] (a : R) : Polynomial.sumIDeriv (Polynomial.C a) = Polynomial.C a

@[simp]

theorem Polynomial.sumIDeriv_X : Polynomial.sumIDeriv Polynomial.X = Polynomial.X + Polynomial.C 1

@[simp]

theorem Polynomial.sumIDeriv_map {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (p : Polynomial R) (f : R →+* S) : Polynomial.sumIDeriv (Polynomial.map f p) = Polynomial.map f (Polynomial.sumIDeriv p)

theorem Polynomial.sumIDeriv_derivative {R : Type u_1} [Semiring R] (p : Polynomial R) : Polynomial.sumIDeriv (Polynomial.derivative p) = Polynomial.derivative (Polynomial.sumIDeriv p)

theorem Polynomial.sumIDeriv_eq_self_add {R : Type u_1} [Semiring R] (p : Polynomial R) : Polynomial.sumIDeriv p = p + Polynomial.sumIDeriv (Polynomial.derivative p)

theorem Polynomial.exists_iterate_derivative_eq_factorial_smul {R : Type u_1} [Semiring R] (p : Polynomial R) (k : ℕ) : ∃ (gp : Polynomial R), gp.natDegree ≤ p.natDegree - k ∧ (⇑Polynomial.derivative)^[k] p = k.factorial • gp

theorem Polynomial.aeval_iterate_derivative_of_lt {R : Type u_1} [CommSemiring R] {A : Type u_3} [CommRing A] [Algebra R A] (p : Polynomial R) (q : ℕ) (r : A) {p' : Polynomial A} (hp : Polynomial.map (algebraMap R A) p = (Polynomial.X - Polynomial.C r) ^ q * p') {k : ℕ} (hk : k < q) : (Polynomial.aeval r) ((⇑Polynomial.derivative)^[k] p) = 0

theorem Polynomial.aeval_iterate_derivative_self {R : Type u_1} [CommSemiring R] {A : Type u_3} [CommRing A] [Algebra R A] (p : Polynomial R) (q : ℕ) (r : A) {p' : Polynomial A} (hp : Polynomial.map (algebraMap R A) p = (Polynomial.X - Polynomial.C r) ^ q * p') : (Polynomial.aeval r) ((⇑Polynomial.derivative)^[q] p) = q.factorial • Polynomial.eval r p'

theorem Polynomial.aeval_iterate_derivative_of_ge {R : Type u_1} [CommSemiring R] (A : Type u_3) [CommRing A] [Algebra R A] (p : Polynomial R) (q : ℕ) {k : ℕ} (hk : q ≤ k) : ∃ (gp : Polynomial R), gp.natDegree ≤ p.natDegree - k ∧ ∀ (r : A), (Polynomial.aeval r) ((⇑Polynomial.derivative)^[k] p) = q.factorial • (Polynomial.aeval r) gp

theorem Polynomial.aeval_sumIDeriv {R : Type u_1} [CommSemiring R] (A : Type u_3) [CommRing A] [Algebra R A] (p : Polynomial R) (q : ℕ) : ∃ (gp : Polynomial R), gp.natDegree ≤ p.natDegree - q ∧ ∀ (r : A) {p' : Polynomial A}, Polynomial.map (algebraMap R A) p = (Polynomial.X - Polynomial.C r) ^ q * p' → (Polynomial.aeval r) (Polynomial.sumIDeriv p) = q.factorial • (Polynomial.aeval r) gp

theorem Polynomial.aeval_sumIDeriv_of_pos {R : Type u_1} [CommSemiring R] (A : Type u_3) [CommRing A] [Algebra R A] [Nontrivial A] [NoZeroDivisors A] (p : Polynomial R) {q : ℕ} (hq : 0 < q) (inj_amap : Function.Injective ⇑(algebraMap R A)) : ∃ (gp : Polynomial R), gp.natDegree ≤ p.natDegree - q ∧ ∀ (r : A) {p' : Polynomial A}, Polynomial.map (algebraMap R A) p = (Polynomial.X - Polynomial.C r) ^ (q - 1) * p' → (Polynomial.aeval r) (Polynomial.sumIDeriv p) = (q - 1).factorial • Polynomial.eval r p' + q.factorial • (Polynomial.aeval r) gp