mathlib3documentation

data.polynomial.hasse_deriv

Hasse derivative of polynomials #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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! * (hasse_deriv 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.hasse_deriv: the k-th Hasse derivative of a polynomial
• polynomial.hasse_deriv_zero: the 0th Hasse derivative is the identity
• polynomial.hasse_deriv_one: the 1st Hasse derivative is the usual derivative
• polynomial.factorial_smul_hasse_deriv: the identity k! • (D k f) = derivative^[k] f
• polynomial.hasse_deriv_comp: the identity (D k).comp (D l) = (k+l).choose k • D (k+l)
• polynomial.hasse_deriv_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_hasse_deriv_eq_zero in data/polynomial/taylor.lean.

Reference #

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

noncomputable def polynomial.hasse_deriv {R : Type u_1} [semiring R] (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.

Equations
theorem polynomial.hasse_deriv_apply {R : Type u_1} [semiring R] (k : ) (f : polynomial R) :
= f.sum (λ (i : ) (r : R), (polynomial.monomial (i - k)) ((i.choose k) * r))
theorem polynomial.hasse_deriv_coeff {R : Type u_1} [semiring R] (k : ) (f : polynomial R) (n : ) :
f).coeff n = ((n + k).choose k) * f.coeff (n + k)
theorem polynomial.hasse_deriv_zero' {R : Type u_1} [semiring R] (f : polynomial R) :
= f
@[simp]
theorem polynomial.hasse_deriv_zero {R : Type u_1} [semiring R] :
theorem polynomial.hasse_deriv_eq_zero_of_lt_nat_degree {R : Type u_1} [semiring R] (p : polynomial R) (n : ) (h : p.nat_degree < n) :
= 0
theorem polynomial.hasse_deriv_one' {R : Type u_1} [semiring R] (f : polynomial R) :
@[simp]
theorem polynomial.hasse_deriv_one {R : Type u_1} [semiring R] :
@[simp]
theorem polynomial.hasse_deriv_monomial {R : Type u_1} [semiring R] (k n : ) (r : R) :
( r) = (polynomial.monomial (n - k)) ((n.choose k) * r)
theorem polynomial.hasse_deriv_C {R : Type u_1} [semiring R] (k : ) (r : R) (hk : 0 < k) :
= 0
theorem polynomial.hasse_deriv_apply_one {R : Type u_1} [semiring R] (k : ) (hk : 0 < k) :
= 0
theorem polynomial.hasse_deriv_X {R : Type u_1} [semiring R] (k : ) (hk : 1 < k) :
theorem polynomial.hasse_deriv_comp {R : Type u_1} [semiring R] (k l : ) :
theorem polynomial.hasse_deriv_mul {R : Type u_1} [semiring R] (k : ) (f g : polynomial R) :
(f * g) = (λ (ij : × ), f * g)