Hasse derivatives of power series

The kth Hasse derivative of a power series f = ∑ aₙ Xⁿ is

D⁽ᵏ⁾ f = ∑ₙ (n + k).choose k • aₙ₊ₖ Xⁿ.

It is defined coefficientwise over any semiring. Only natural-number multiples of coefficients occur, so the coefficients need not commute; this allows Hasse derivatives of series with coefficients in a noncommutative algebra, such as an algebra of operators. Over a commutative semiring, k! • D⁽ᵏ⁾ = (d/dX)^[k]. Unlike (d/dX)^[k] / k!, the Hasse derivative needs no division by k!, so it keeps its meaning in positive characteristic.

The definitions and lemmas parallel Mathlib's Polynomial.hasseDeriv, and on polynomials the two agree (PowerSeries.hasseDeriv_coe). Since a coefficient of a Hasse derivative of f only sees finitely many coefficients of f (PowerSeries.trunc_hasseDeriv), the Leibniz rule is deduced from Mathlib's polynomial Leibniz rule Polynomial.hasseDeriv_mul.

Main definitions

• PowerSeries.hasseDeriv: the kth Hasse derivative, an R-linear map R⟦X⟧ → R⟦X⟧.

Main results

• PowerSeries.coeff_hasseDeriv: coeff n (D⁽ᵏ⁾ f) = (n + k).choose k * coeff (n + k) f.
• PowerSeries.hasseDeriv_coe and PowerSeries.trunc_hasseDeriv: comparison with Polynomial.hasseDeriv on polynomials and on truncations.
• PowerSeries.hasseDeriv_map: Hasse derivatives commute with coefficient maps.
• PowerSeries.hasseDeriv_comp: D⁽ᵏ⁾ ∘ D⁽ˡ⁾ = (k + l).choose k • D⁽ᵏ⁺ˡ⁾.
• PowerSeries.hasseDeriv_mul: the Leibniz rule D⁽ᵏ⁾ (f * g) = ∑_{i + j = k} D⁽ⁱ⁾ f * D⁽ʲ⁾ g, with the factors in their original order.
• PowerSeries.hasseDeriv_succ_X_mul and PowerSeries.hasseDeriv_succ_X_sub_C_mul: its special case D⁽ᵏ⁺¹⁾ ((X - a) * f) = (X - a) * D⁽ᵏ⁺¹⁾ f + D⁽ᵏ⁾ f.
• PowerSeries.hasseDeriv_one_apply and PowerSeries.factorial_smul_hasseDeriv: over a commutative semiring, D⁽¹⁾ = d/dX and k! • D⁽ᵏ⁾ = (d/dX)^[k].

References

• H. Hasse, Theorie der höheren Differentiale in einem algebraischen Funktionenkörper mit vollkommenem Konstantenkörper bei beliebiger Charakteristik, J. Reine Angew. Math. 175 (1936).

noncomputable def PowerSeries.hasseDeriv {R : Type u_1} [Semiring R] (k : ℕ) : PowerSeries R →ₗ[R] PowerSeries R

The kth Hasse derivative of a power series ∑ aₙ Xⁿ is ∑ (n + k).choose k • aₙ₊ₖ Xⁿ. Over a commutative semiring, k! • hasseDeriv k f is the kth iterated derivative of f (PowerSeries.factorial_smul_hasseDeriv).

@[simp]

theorem PowerSeries.coeff_hasseDeriv {R : Type u_1} [Semiring R] (k : ℕ) (f : PowerSeries R) (n : ℕ) : (coeff n) ((hasseDeriv k) f) = ↑((n + k).choose k) * (coeff (n + k)) f

The coefficients of a Hasse derivative: coeff n (D⁽ᵏ⁾ f) = (n + k).choose k * coeff (n + k) f.

@[simp]

theorem PowerSeries.hasseDeriv_zero {R : Type u_1} [Semiring R] : hasseDeriv 0 = LinearMap.id

The 0th Hasse derivative is the identity.

@[simp]

theorem PowerSeries.hasseDeriv_coe {R : Type u_1} [Semiring R] (k : ℕ) (p : Polynomial R) : (hasseDeriv k) ↑p = ↑((Polynomial.hasseDeriv k) p)

On polynomials, the Hasse derivative of power series is Polynomial.hasseDeriv.

theorem PowerSeries.trunc_hasseDeriv {R : Type u_1} [Semiring R] (k : ℕ) (f : PowerSeries R) (n : ℕ) : (trunc n) ((hasseDeriv k) f) = (Polynomial.hasseDeriv k) ((trunc (n + k)) f)

The coefficients of D⁽ᵏ⁾ f below n only depend on the coefficients of f below n + k.

@[simp]

theorem PowerSeries.hasseDeriv_monomial {R : Type u_1} [Semiring R] (k n : ℕ) (a : R) : (hasseDeriv k) ((monomial n) a) = (monomial (n - k)) (↑(n.choose k) * a)

The Hasse derivative of a monomial: D⁽ᵏ⁾ (a Xⁿ) = n.choose k * a Xⁿ⁻ᵏ.

theorem PowerSeries.hasseDeriv_C {R : Type u_1} [Semiring R] {k : ℕ} (hk : 0 < k) (a : R) : (hasseDeriv k) (C a) = 0

Positive Hasse derivatives vanish on constants.

@[simp]

theorem PowerSeries.hasseDeriv_map {R : Type u_1} [Semiring R] (k : ℕ) {S : Type u_2} [Semiring S] (φ : R →+* S) (f : PowerSeries R) : (hasseDeriv k) ((map φ) f) = (map φ) ((hasseDeriv k) f)

Hasse derivatives commute with coefficient maps.

theorem PowerSeries.hasseDeriv_comp {R : Type u_1} [Semiring R] (k l : ℕ) : hasseDeriv k ∘ₗ hasseDeriv l = (k + l).choose k • hasseDeriv (k + l)

The composition of Hasse derivatives: D⁽ᵏ⁾ ∘ D⁽ˡ⁾ = (k + l).choose k • D⁽ᵏ⁺ˡ⁾.

theorem PowerSeries.hasseDeriv_mul {R : Type u_1} [Semiring R] (k : ℕ) (f g : PowerSeries R) : (hasseDeriv k) (f * g) = ∑ ij ∈ Finset.antidiagonal k, (hasseDeriv ij.1) f * (hasseDeriv ij.2) g

The Leibniz rule for Hasse derivatives: D⁽ᵏ⁾ (f * g) = ∑_{i + j = k} D⁽ⁱ⁾ f * D⁽ʲ⁾ g. The coefficients need not commute.

theorem PowerSeries.hasseDeriv_succ_X_mul {R : Type u_1} [Semiring R] (k : ℕ) (f : PowerSeries R) : (hasseDeriv (k + 1)) (X * f) = X * (hasseDeriv (k + 1)) f + (hasseDeriv k) f

The Leibniz rule for a product with X: D⁽ᵏ⁺¹⁾ (X * f) = X * D⁽ᵏ⁺¹⁾ f + D⁽ᵏ⁾ f.

theorem PowerSeries.hasseDeriv_succ_X_sub_C_mul {R : Type u_1} [Ring R] (k : ℕ) (a : R) (f : PowerSeries R) : (hasseDeriv (k + 1)) ((X - C a) * f) = (X - C a) * (hasseDeriv (k + 1)) f + (hasseDeriv k) f

The Leibniz rule for a product with X - a: D⁽ᵏ⁺¹⁾ ((X - a) * f) = (X - a) * D⁽ᵏ⁺¹⁾ f + D⁽ᵏ⁾ f.

@[simp]

theorem PowerSeries.hasseDeriv_one_apply {R : Type u_1} [CommSemiring R] (f : PowerSeries R) : (hasseDeriv 1) f = derivative f

The first Hasse derivative is the derivative.

theorem PowerSeries.factorial_smul_hasseDeriv {R : Type u_1} [CommSemiring R] (k : ℕ) (f : PowerSeries R) : k.factorial • (hasseDeriv k) f = (⇑derivative)^[k] f

k! times the kth Hasse derivative is the kth iterated derivative: k! • D⁽ᵏ⁾ f = (d/dX)^[k] f.