Documentation

Mathlib.Algebra.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.

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/

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
Instances For
    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)
    @[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) :
    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) :
    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.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