Hasse derivatives of multivariate power series

For a multi-index d : σ →₀ ℕ, the d-th Hasse derivative of a multivariate power series f = ∑ₘ aₘ Xᵐ is

∂^d f = ∑ₘ (∏ⱼ (mⱼ + dⱼ choose dⱼ)) • aₘ₊d Xᵐ.

It is defined coefficientwise over any semiring: only natural-number multiples of coefficients occur, so the coefficients need not commute. Unlike (∂/∂X)^d / d!, it needs no division by factorials, so it keeps its meaning in positive characteristic; in a single variable Xᵢ, k! • ∂^(k eᵢ) is the k-th iterated partial derivative. The coefficient formula, the values on monomials, the composition rule and commutation hold over any semiring.

On polynomials, ∂^d is MvPolynomial.hasseDeriv, whose values are the Taylor coefficients of a polynomial (MvPolynomial.coeff_taylor_X_map_C). Since a coefficient of ∂^d f only sees finitely many coefficients of f, the Leibniz rule is deduced from the polynomial Leibniz rule MvPolynomial.hasseDeriv_mul; like the comparison with polynomials and with partial derivatives, it is stated over commutative semirings, where MvPolynomial and MvPowerSeries.pderiv live. The definitions and lemmas parallel the one-variable PowerSeries.hasseDeriv and the polynomial MvPolynomial.hasseDeriv. Hasse derivatives act on restricted power series at every positive polyradius (TauCeti.RingTheory.MvPowerSeries.HasseDeriv.GaussNorm).

Main definitions

• MvPowerSeries.hasseDeriv d: the d-th Hasse derivative, an R-linear endomorphism of MvPowerSeries σ R.

Main results

• MvPowerSeries.coeff_hasseDeriv: [Xᵐ] ∂^d f = (∏ⱼ (mⱼ + dⱼ choose dⱼ)) [X^(m + d)] f.
• MvPowerSeries.hasseDeriv_monomial, MvPowerSeries.hasseDeriv_C: values on monomials and constants.
• MvPowerSeries.hasseDeriv_map: Hasse derivatives commute with coefficient maps.
• MvPowerSeries.hasseDeriv_comp: ∂^a ∘ ∂^b = (∏ⱼ (aⱼ + bⱼ choose aⱼ)) • ∂^(a + b), and MvPowerSeries.hasseDeriv_comm: Hasse derivatives commute with each other.
• MvPowerSeries.hasseDeriv_coe and MvPowerSeries.trunc'_hasseDeriv: comparison with MvPolynomial.hasseDeriv on polynomials and on truncations.
• MvPowerSeries.hasseDeriv_mul: the Leibniz rule ∂^d (f g) = ∑_{a + b = d} ∂^a f · ∂^b g.
• MvPowerSeries.factorial_smul_hasseDeriv_single: k! • ∂^(k eᵢ) f = (∂/∂Xᵢ)^[k] f.
• PowerSeries.hasseDeriv_eq_mvPowerSeries_hasseDeriv: on R⟦X⟧ = MvPowerSeries Unit R, PowerSeries.hasseDeriv k is MvPowerSeries.hasseDeriv (single () 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 MvPowerSeries.hasseDeriv {σ : Type u_1} {R : Type u_2} [Semiring R] (d : σ →₀ ℕ) : MvPowerSeries σ R →ₗ[R] MvPowerSeries σ R

The d-th Hasse derivative ∂^d of a multivariate power series, the R-linear map with [Xᵐ] ∂^d f = (∏ⱼ (mⱼ + dⱼ choose dⱼ)) [X^(m + d)] f. Over a commutative semiring, in a single variable Xᵢ, k! • ∂^(k eᵢ) is the k-th iterated partial derivative (MvPowerSeries.factorial_smul_hasseDeriv_single).

@[simp]

theorem MvPowerSeries.coeff_hasseDeriv {σ : Type u_1} {R : Type u_2} [Semiring R] (d m : σ →₀ ℕ) (f : MvPowerSeries σ R) : (coeff m) ((hasseDeriv d) f) = ↑(d.prod fun (j : σ) (k : ℕ) => (m j + k).choose k) * (coeff (m + d)) f

The coefficients of a Hasse derivative: [Xᵐ] ∂^d f = (∏ⱼ (mⱼ + dⱼ choose dⱼ)) [X^(m + d)] f.

@[simp]

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

The 0-th Hasse derivative is the identity.

@[simp]

theorem MvPowerSeries.hasseDeriv_monomial {σ : Type u_1} {R : Type u_2} [Semiring R] (d m : σ →₀ ℕ) (a : R) : (hasseDeriv d) ((monomial m) a) = (monomial (m - d)) (↑(d.prod fun (j : σ) (k : ℕ) => (m j).choose k) * a)

The Hasse derivative of a monomial: ∂^d (a Xᵐ) = (∏ⱼ (mⱼ choose dⱼ)) a X^(m - d). The coefficient vanishes unless d ≤ m.

@[simp]

theorem MvPowerSeries.hasseDeriv_C {σ : Type u_1} {R : Type u_2} [Semiring R] {d : σ →₀ ℕ} (hd : d ≠ 0) (a : R) : (hasseDeriv d) (C a) = 0

Every Hasse derivative of positive order kills constants.

@[simp]

theorem MvPowerSeries.hasseDeriv_one {σ : Type u_1} {R : Type u_2} [Semiring R] {d : σ →₀ ℕ} (hd : d ≠ 0) : (hasseDeriv d) 1 = 0

Every Hasse derivative of positive order kills the constant series 1.

@[simp]

theorem MvPowerSeries.hasseDeriv_map {σ : Type u_1} {R : Type u_2} [Semiring R] {S : Type u_3} [Semiring S] (φ : R →+* S) (d : σ →₀ ℕ) (f : MvPowerSeries σ R) : (hasseDeriv d) ((map φ) f) = (map φ) ((hasseDeriv d) f)

Hasse derivatives commute with coefficient maps.

theorem MvPowerSeries.hasseDeriv_comp {σ : Type u_1} {R : Type u_2} [Semiring R] (a b : σ →₀ ℕ) : hasseDeriv a ∘ₗ hasseDeriv b = (a.prod fun (j : σ) (k : ℕ) => (k + b j).choose k) • hasseDeriv (a + b)

The composition rule ∂^a ∘ ∂^b = (∏ⱼ (aⱼ + bⱼ choose aⱼ)) • ∂^(a + b).

theorem MvPowerSeries.hasseDeriv_comm {σ : Type u_1} {R : Type u_2} [Semiring R] (a b : σ →₀ ℕ) : hasseDeriv a ∘ₗ hasseDeriv b = hasseDeriv b ∘ₗ hasseDeriv a

Hasse derivatives commute: ∂^a ∘ ∂^b = ∂^b ∘ ∂^a. In particular Hasse derivatives in different variables commute.

@[simp]

theorem MvPowerSeries.hasseDeriv_coe {σ : Type u_1} {R : Type u_2} [CommSemiring R] (d : σ →₀ ℕ) (P : MvPolynomial σ R) : (hasseDeriv d) ↑P = ↑((MvPolynomial.hasseDeriv d) P)

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

theorem MvPowerSeries.trunc'_hasseDeriv {σ : Type u_1} {R : Type u_2} [CommSemiring R] [DecidableEq σ] (n d : σ →₀ ℕ) (f : MvPowerSeries σ R) : (trunc' R n) ((hasseDeriv d) f) = (MvPolynomial.hasseDeriv d) ((trunc' R (n + d)) f)

The coefficients of ∂^d f of exponent at most n only depend on the coefficients of f of exponent at most n + d.

theorem MvPowerSeries.hasseDeriv_mul {σ : Type u_1} {R : Type u_2} [CommSemiring R] [DecidableEq σ] (d : σ →₀ ℕ) (f g : MvPowerSeries σ R) : (hasseDeriv d) (f * g) = ∑ x ∈ Finset.antidiagonal d, (hasseDeriv x.1) f * (hasseDeriv x.2) g

The Leibniz rule for Hasse derivatives: ∂^d (f g) = ∑_{a + b = d} ∂^a f · ∂^b g.

@[simp]

theorem MvPowerSeries.pderiv_hasseDeriv_single {σ : Type u_1} {R : Type u_2} [CommSemiring R] (i : σ) (k : ℕ) (f : MvPowerSeries σ R) : (pderiv i) ((hasseDeriv (Finsupp.single i k)) f) = (k + 1) • (hasseDeriv (Finsupp.single i (k + 1))) f

Differentiating ∂^(k eᵢ) f in Xᵢ gives (k + 1) ∂^((k + 1) eᵢ) f.

theorem MvPowerSeries.factorial_smul_hasseDeriv_single {σ : Type u_1} {R : Type u_2} [CommSemiring R] (i : σ) (k : ℕ) (f : MvPowerSeries σ R) : k.factorial • (hasseDeriv (Finsupp.single i k)) f = (⇑(pderiv i))^[k] f

The Hasse derivative ∂^(k eᵢ) is the k-th partial derivative in Xᵢ divided by k!: k! • ∂^(k eᵢ) f = (∂/∂Xᵢ)^[k] f.

@[simp]

theorem MvPowerSeries.hasseDeriv_single_one {σ : Type u_1} {R : Type u_2} [CommSemiring R] (i : σ) (f : MvPowerSeries σ R) : (hasseDeriv (Finsupp.single i 1)) f = (pderiv i) f

The first Hasse derivative in Xᵢ is the partial derivative in Xᵢ.

theorem PowerSeries.hasseDeriv_eq_mvPowerSeries_hasseDeriv {R : Type u_1} [Semiring R] (k : ℕ) (f : PowerSeries R) : (hasseDeriv k) f = (MvPowerSeries.hasseDeriv (Finsupp.single () k)) f

On R⟦X⟧ = MvPowerSeries Unit R, the k-th Hasse derivative of power series is the multivariate Hasse derivative of multi-index single () k.