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} [Semiring R] (k : ℕ) : Polynomial R →ₗ[R] Polynomial R

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.

Equations

• Polynomial.hasseDeriv k = Polynomial.lsum fun (i : ℕ) => Polynomial.monomial (i - k) ∘ₗ DistribMulAction.toLinearMap R R (i.choose k)

theorem Polynomial.hasseDeriv_apply {R : Type u_1} [Semiring R] (k : ℕ) (f : Polynomial R) : (Polynomial.hasseDeriv k) f = f.sum fun (i : ℕ) (r : R) => (Polynomial.monomial (i - k)) (↑(i.choose k) * r)

theorem Polynomial.hasseDeriv_coeff {R : Type u_1} [Semiring R] (k : ℕ) (f : Polynomial R) (n : ℕ) : ((Polynomial.hasseDeriv k) f).coeff n = ↑((n + k).choose k) * f.coeff (n + k)

theorem Polynomial.hasseDeriv_zero' {R : Type u_1} [Semiring R] (f : Polynomial R) : (Polynomial.hasseDeriv 0) f = f

@[simp]

theorem Polynomial.hasseDeriv_zero {R : Type u_1} [Semiring R] : Polynomial.hasseDeriv 0 = LinearMap.id

theorem Polynomial.hasseDeriv_eq_zero_of_lt_natDegree {R : Type u_1} [Semiring R] (p : Polynomial R) (n : ℕ) (h : p.natDegree < n) : (Polynomial.hasseDeriv n) p = 0

theorem Polynomial.hasseDeriv_one' {R : Type u_1} [Semiring R] (f : Polynomial R) : (Polynomial.hasseDeriv 1) f = Polynomial.derivative f

@[simp]

theorem Polynomial.hasseDeriv_one {R : Type u_1} [Semiring R] : Polynomial.hasseDeriv 1 = Polynomial.derivative

@[simp]

theorem Polynomial.hasseDeriv_monomial {R : Type u_1} [Semiring R] (k : ℕ) (n : ℕ) (r : R) : (Polynomial.hasseDeriv k) ((Polynomial.monomial n) r) = (Polynomial.monomial (n - k)) (↑(n.choose k) * r)

theorem Polynomial.hasseDeriv_C {R : Type u_1} [Semiring R] (k : ℕ) (r : R) (hk : 0 < k) : (Polynomial.hasseDeriv k) (Polynomial.C r) = 0

theorem Polynomial.hasseDeriv_apply_one {R : Type u_1} [Semiring R] (k : ℕ) (hk : 0 < k) : (Polynomial.hasseDeriv k) 1 = 0

theorem Polynomial.hasseDeriv_X {R : Type u_1} [Semiring R] (k : ℕ) (hk : 1 < k) : (Polynomial.hasseDeriv k) Polynomial.X = 0

theorem Polynomial.factorial_smul_hasseDeriv {R : Type u_1} [Semiring R] (k : ℕ) : ⇑(k.factorial • Polynomial.hasseDeriv k) = (⇑Polynomial.derivative)^[k]

theorem Polynomial.hasseDeriv_comp {R : Type u_1} [Semiring R] (k : ℕ) (l : ℕ) : Polynomial.hasseDeriv k ∘ₗ Polynomial.hasseDeriv l = (k + l).choose k • Polynomial.hasseDeriv (k + l)

theorem Polynomial.natDegree_hasseDeriv_le {R : Type u_1} [Semiring R] (p : Polynomial R) (n : ℕ) : ((Polynomial.hasseDeriv n) p).natDegree ≤ p.natDegree - n

theorem Polynomial.natDegree_hasseDeriv {R : Type u_1} [Semiring R] [NoZeroSMulDivisors ℕ R] (p : Polynomial R) (n : ℕ) : ((Polynomial.hasseDeriv n) p).natDegree = p.natDegree - n

theorem Polynomial.hasseDeriv_mul {R : Type u_1} [Semiring R] (k : ℕ) (f : Polynomial R) (g : Polynomial R) : (Polynomial.hasseDeriv k) (f * g) = (Finset.antidiagonal k).sum fun (ij : ℕ × ℕ) => (Polynomial.hasseDeriv ij.1) f * (Polynomial.hasseDeriv ij.2) g