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 mapPolynomial.sumIDeriv_apply
,Polynomial.sumIDeriv_apply_of_lt
,Polynomial.sumIDeriv_apply_of_le
:Polynomial.sumIDeriv
expressed as a sumPolynomial.sumIDeriv_C
,Polynomial.sumIDeriv_X
:Polynomial.sumIDeriv
applied to simple polynomialsPolynomial.sumIDeriv_map
:Polynomial.sumIDeriv
commutes withPolynomial.map
Polynomial.sumIDeriv_derivative
:Polynomial.sumIDeriv
commutes withPolynomial.derivative
Polynomial.sumIDeriv_eq_self_add
:sumIDeriv p = p + sumIDeriv (derivative p)
Polynomial.exists_iterate_derivative_eq_factorial_smul
: thek
'th iterated derivative of a polynomial has a common factork!
Polynomial.aeval_iterate_derivative_of_lt
,Polynomial.aeval_iterate_derivative_self
,Polynomial.aeval_iterate_derivative_of_ge
: applyingPolynomial.aeval
to iterated derivativesPolynomial.aeval_sumIDeriv
,Polynomial.aeval_sumIDeriv_of_pos
: applyingPolynomial.aeval
toPolynomial.sumIDeriv
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
Instances For
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]
@[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.exists_iterate_derivative_eq_factorial_smul
{R : Type u_1}
[Semiring R]
(p : Polynomial R)
(k : ℕ)
:
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)
:
∃ (gp : Polynomial R),
gp.natDegree ≤ p.natDegree - q ∧ (Function.Injective ⇑(algebraMap R A) →
∀ (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)