# Documentation

Mathlib.Data.Polynomial.HasseDeriv

# Hasse derivative of polynomials #

The kth 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! * (hasseDeriv 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.hasseDeriv: the k-th Hasse derivative of a polynomial
• Polynomial.hasseDeriv_zero: the 0th Hasse derivative is the identity
• Polynomial.hasseDeriv_one: the 1st Hasse derivative is the usual derivative
• Polynomial.factorial_smul_hasseDeriv: the identity k! • (D k f) = derivative^[k] f
• Polynomial.hasseDeriv_comp: the identity (D k).comp (D l) = (k+l).choose k • D (k+l)
• Polynomial.hasseDeriv_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_hasseDeriv_eq_zero in Data/Polynomial/Taylor.lean.

## Reference #

https://math.fontein.de/2009/08/12/the-hasse-derivative/

def Polynomial.hasseDeriv {R : Type u_1} [] (k : ) :

The kth 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.

Instances For
theorem Polynomial.hasseDeriv_apply {R : Type u_1} [] (k : ) (f : ) :
↑() f = Polynomial.sum f fun i r => ↑(Polynomial.monomial (i - k)) (↑() * r)
theorem Polynomial.hasseDeriv_coeff {R : Type u_1} [] (k : ) (f : ) (n : ) :
Polynomial.coeff (↑() f) n = ↑(Nat.choose (n + k) k) * Polynomial.coeff f (n + k)
theorem Polynomial.hasseDeriv_zero' {R : Type u_1} [] (f : ) :
↑() f = f
@[simp]
theorem Polynomial.hasseDeriv_zero {R : Type u_1} [] :
= LinearMap.id
theorem Polynomial.hasseDeriv_eq_zero_of_lt_natDegree {R : Type u_1} [] (p : ) (n : ) (h : ) :
↑() p = 0
theorem Polynomial.hasseDeriv_one' {R : Type u_1} [] (f : ) :
↑() f = Polynomial.derivative f
@[simp]
theorem Polynomial.hasseDeriv_one {R : Type u_1} [] :
= Polynomial.derivative
@[simp]
theorem Polynomial.hasseDeriv_monomial {R : Type u_1} [] (k : ) (n : ) (r : R) :
↑() (↑() r) = ↑(Polynomial.monomial (n - k)) (↑() * r)
theorem Polynomial.hasseDeriv_C {R : Type u_1} [] (k : ) (r : R) (hk : 0 < k) :
↑() (Polynomial.C r) = 0
theorem Polynomial.hasseDeriv_apply_one {R : Type u_1} [] (k : ) (hk : 0 < k) :
↑() 1 = 0
theorem Polynomial.hasseDeriv_X {R : Type u_1} [] (k : ) (hk : 1 < k) :
↑() Polynomial.X = 0
theorem Polynomial.factorial_smul_hasseDeriv {R : Type u_1} [] (k : ) :
↑() = (Polynomial.derivative)^[k]
theorem Polynomial.hasseDeriv_comp {R : Type u_1} [] (k : ) (l : ) :
theorem Polynomial.natDegree_hasseDeriv_le {R : Type u_1} [] (p : ) (n : ) :
theorem Polynomial.natDegree_hasseDeriv {R : Type u_1} [] [] (p : ) (n : ) :
theorem Polynomial.hasseDeriv_mul {R : Type u_1} [] (k : ) (f : ) (g : ) :
↑() (f * g) = Finset.sum () fun ij => ↑(Polynomial.hasseDeriv ij.fst) f * ↑(Polynomial.hasseDeriv ij.snd) g