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.

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 : ℕ) :

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.hasse_deriv k = polynomial.lsum (λ (i : ℕ), (polynomial.monomial (i - k)).comp (distrib_mul_action.to_linear_map R R (i.choose k)))

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)

theorem polynomial.hasse_deriv_zero' {R : Type u_1} [semiring R] (f : polynomial R) :

⇑(polynomial.hasse_deriv 0) f = f

@[simp]

theorem polynomial.hasse_deriv_zero {R : Type u_1} [semiring R] :

polynomial.hasse_deriv 0 = linear_map.id

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) :

⇑(polynomial.hasse_deriv n) p = 0

theorem polynomial.hasse_deriv_one' {R : Type u_1} [semiring R] (f : polynomial R) :

⇑(polynomial.hasse_deriv 1) f = ⇑polynomial.derivative f

@[simp]

theorem polynomial.hasse_deriv_one {R : Type u_1} [semiring R] :

polynomial.hasse_deriv 1 = polynomial.derivative

@[simp]

theorem polynomial.hasse_deriv_monomial {R : Type u_1} [semiring R] (k n : ℕ) (r : R) :

⇑(polynomial.hasse_deriv k) (⇑(polynomial.monomial n) 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) :

⇑(polynomial.hasse_deriv k) (⇑polynomial.C r) = 0

theorem polynomial.hasse_deriv_apply_one {R : Type u_1} [semiring R] (k : ℕ) (hk : 0 < k) :

⇑(polynomial.hasse_deriv k) 1 = 0

theorem polynomial.hasse_deriv_X {R : Type u_1} [semiring R] (k : ℕ) (hk : 1 < k) :

⇑(polynomial.hasse_deriv k) polynomial.X = 0

theorem polynomial.factorial_smul_hasse_deriv {R : Type u_1} [semiring R] (k : ℕ) :

⇑(k.factorial • polynomial.hasse_deriv k) = (⇑polynomial.derivative ^[k])

theorem polynomial.hasse_deriv_comp {R : Type u_1} [semiring R] (k l : ℕ) :

(polynomial.hasse_deriv k).comp (polynomial.hasse_deriv l) = (k + l).choose k • polynomial.hasse_deriv (k + l)

theorem polynomial.nat_degree_hasse_deriv_le {R : Type u_1} [semiring R] (p : polynomial R) (n : ℕ) :

(⇑(polynomial.hasse_deriv n) p).nat_degree ≤ p.nat_degree - n

theorem polynomial.nat_degree_hasse_deriv {R : Type u_1} [semiring R] [no_zero_smul_divisors ℕ R] (p : polynomial R) (n : ℕ) :

(⇑(polynomial.hasse_deriv n) p).nat_degree = p.nat_degree - n

theorem polynomial.hasse_deriv_mul {R : Type u_1} [semiring R] (k : ℕ) (f g : polynomial R) :

⇑(polynomial.hasse_deriv k) (f * g) = (finset.nat.antidiagonal k).sum (λ (ij : ℕ × ℕ), ⇑(polynomial.hasse_deriv ij.fst) f * ⇑(polynomial.hasse_deriv ij.snd) g)