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.

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

theorem Polynomial.hasseDeriv_coeff {R : Type u_1} [Semiring R] (k : ℕ) (f : Polynomial R) (n : ℕ) : Polynomial.coeff (↑(Polynomial.hasseDeriv k) f) n = ↑(Nat.choose (n + k) k) * Polynomial.coeff f (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 : Polynomial.natDegree p < 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)) (↑(Nat.choose n 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 : ℕ) : ↑(Nat.factorial k • Polynomial.hasseDeriv k) = (↑Polynomial.derivative)^[k]

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

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

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

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