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 ∈ antidiagonal k, D ij.1 f * D ij.2 g

For the identity principle, see Polynomial.eq_zero_of_hasseDeriv_eq_zero in Mathlib/Algebra/Polynomial/Taylor.lean.

Reference

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

noncomputable 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) ∘ₗ DistribSMul.toLinearMap R R (i.choose k)

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

theorem Polynomial.hasseDeriv_coeff {R : Type u_1} [Semiring R] (k : ℕ) (f : Polynomial R) (n : ℕ) : ((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) : (hasseDeriv 0) f = f

@[simp]

theorem Polynomial.hasseDeriv_zero {R : Type u_1} [Semiring R] : 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) : (hasseDeriv n) p = 0

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

@[simp]

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

@[simp]

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

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

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

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

@[simp]

theorem Polynomial.hasseDeriv_map {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] (f : R →+* S) (k : ℕ) (p : Polynomial R) : (hasseDeriv k) (map f p) = map f ((hasseDeriv k) p)

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

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

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

theorem Polynomial.hasseDeriv_natDegree_eq_C {R : Type u_1} [Semiring R] (f : Polynomial R) : (hasseDeriv f.natDegree) f = C f.leadingCoeff

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

theorem Polynomial.hasseDeriv_mul {R : Type u_1} [Semiring R] (k : ℕ) (f g : Polynomial R) : (hasseDeriv k) (f * g) = ∑ ij ∈ Finset.antidiagonal k, (hasseDeriv ij.1) f * (hasseDeriv ij.2) g