Hasse derivative of polynomials #
The k
th Hasse derivative of a polynomial ∑ a_i X^i
is ∑ (i.choose k) a_i X^(i-k)
.
It is a variant of the usual derivative, and satisfies k! * (hasse_deriv k f) = derivative^[k] f
.
The main benefit is that is gives an atomic way of talking about expressions such as
(derivative^[k] f).eval r / k!
, that occur in Taylor expansions, for example.
Main declarations #
In the following, we write D k
for the k
-th Hasse derivative hasse_deriv k
.
polynomial.hasse_deriv
: thek
-th Hasse derivative of a polynomialpolynomial.hasse_deriv_zero
: the0
th Hasse derivative is the identitypolynomial.hasse_deriv_one
: the1
st Hasse derivative is the usual derivativepolynomial.factorial_smul_hasse_deriv
: the identityk! • (D k f) = derivative^[k] f
polynomial.hasse_deriv_comp
: the identity(D k).comp (D l) = (k+l).choose k • D (k+l)
polynomial.hasse_deriv_mul
: the "Leibniz rule"D k (f * g) = ∑ ij in antidiagonal k, D ij.1 f * D ij.2 g
For the identity principle, see polynomial.eq_zero_of_hasse_deriv_eq_zero
in data/polynomial/taylor.lean
.
Reference #
noncomputable
def
polynomial.hasse_deriv
{R : Type u_1}
[semiring R]
(k : ℕ) :
polynomial R →ₗ[R] polynomial R
The k
th Hasse derivative of a polynomial ∑ a_i X^i
is ∑ (i.choose k) a_i X^(i-k)
.
It satisfies k! * (hasse_deriv k f) = derivative^[k] f
.
Equations
- polynomial.hasse_deriv k = polynomial.lsum (λ (i : ℕ), (polynomial.monomial (i - k)).comp (distrib_mul_action.to_linear_map R R (i.choose k)))
theorem
polynomial.hasse_deriv_zero'
{R : Type u_1}
[semiring R]
(f : polynomial R) :
⇑(polynomial.hasse_deriv 0) f = f
@[simp]
theorem
polynomial.hasse_deriv_eq_zero_of_lt_nat_degree
{R : Type u_1}
[semiring R]
(p : polynomial R)
(n : ℕ)
(h : p.nat_degree < n) :
⇑(polynomial.hasse_deriv n) p = 0
@[simp]
@[simp]
theorem
polynomial.hasse_deriv_monomial
{R : Type u_1}
[semiring R]
(k n : ℕ)
(r : R) :
⇑(polynomial.hasse_deriv k) (⇑(polynomial.monomial n) r) = ⇑(polynomial.monomial (n - k)) (↑(n.choose k) * r)
theorem
polynomial.hasse_deriv_C
{R : Type u_1}
[semiring R]
(k : ℕ)
(r : R)
(hk : 0 < k) :
⇑(polynomial.hasse_deriv k) (⇑polynomial.C r) = 0
theorem
polynomial.hasse_deriv_apply_one
{R : Type u_1}
[semiring R]
(k : ℕ)
(hk : 0 < k) :
⇑(polynomial.hasse_deriv k) 1 = 0
theorem
polynomial.hasse_deriv_comp
{R : Type u_1}
[semiring R]
(k l : ℕ) :
(polynomial.hasse_deriv k).comp (polynomial.hasse_deriv l) = (k + l).choose k • polynomial.hasse_deriv (k + l)
theorem
polynomial.nat_degree_hasse_deriv_le
{R : Type u_1}
[semiring R]
(p : polynomial R)
(n : ℕ) :
(⇑(polynomial.hasse_deriv n) p).nat_degree ≤ p.nat_degree - n
theorem
polynomial.nat_degree_hasse_deriv
{R : Type u_1}
[semiring R]
[no_zero_smul_divisors ℕ R]
(p : polynomial R)
(n : ℕ) :
(⇑(polynomial.hasse_deriv n) p).nat_degree = p.nat_degree - n
theorem
polynomial.hasse_deriv_mul
{R : Type u_1}
[semiring R]
(k : ℕ)
(f g : polynomial R) :
⇑(polynomial.hasse_deriv k) (f * g) = (finset.nat.antidiagonal k).sum (λ (ij : ℕ × ℕ), ⇑(polynomial.hasse_deriv ij.fst) f * ⇑(polynomial.hasse_deriv ij.snd) g)