mathlib3 documentation

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.

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) :
(polynomial.hasse_deriv k) f = 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 : ) :
((polynomial.hasse_deriv k) f).coeff n = ((n + k).choose k) * f.coeff (n + k)
@[simp]
theorem polynomial.hasse_deriv_C {R : Type u_1} [semiring R] (k : ) (r : R) (hk : 0 < k) :
theorem polynomial.hasse_deriv_apply_one {R : Type u_1} [semiring R] (k : ) (hk : 0 < k) :
theorem polynomial.hasse_deriv_X {R : Type u_1} [semiring R] (k : ) (hk : 1 < k) :