Hasse derivatives of multivariate polynomials

For a multi-index d : σ →₀ ℕ, the d-th Hasse (divided) partial derivative ∂^d of a multivariate polynomial sends the monomial X^m to (∏ⱼ (mⱼ choose dⱼ)) X^(m - d), which is zero unless d ≤ m. It is defined over any commutative semiring, so it preserves integrality of coefficients, and in a single variable k! • ∂^(k eᵢ) is the k-th partial derivative in Xᵢ (MvPolynomial.factorial_smul_hasseDeriv_single).

Hasse derivatives are the Taylor coefficients of a polynomial: P(X + Y) = ∑_d (∂^d P)(X) Y^d (see TauCeti.RingTheory.MvPolynomial.HasseDeriv.Taylor). They are the jets used to measure the vanishing of auxiliary polynomials at a point, as in the index of a polynomial in the proof of Roth's theorem.

Main definitions

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

Main results

• MvPolynomial.hasseDeriv_monomial, MvPolynomial.hasseDeriv_coeff: the values on monomials and the coefficients [X^m] ∂^d P = (∏ⱼ (mⱼ + dⱼ choose dⱼ)) [X^(m + d)] P.
• MvPolynomial.eval_const_hasseDeriv_monomial: the jet ∂^d (a X^m) at a diagonal point (x, …, x).
• MvPolynomial.abv_coeff_hasseDeriv_le: for an absolute value v, v([X^m] ∂^d P) ≤ 2 ^ |m + d| v([X^(m + d)] P); with partial degrees ≤ rᵢ the factor is at most 2 ^ ∑ᵢ rᵢ (MvPolynomial.abv_coeff_hasseDeriv_le_of_degreeOf_le), with coefficients also bounded by B this is MvPolynomial.abv_coeff_hasseDeriv_le_two_pow_mul, and at a nonarchimedean v the factor 2 ^ |m + d| disappears (MvPolynomial.abv_coeff_hasseDeriv_le_of_isNonarchimedean).
• MvPolynomial.hasseDeriv_zero, MvPolynomial.hasseDeriv_C, MvPolynomial.hasseDeriv_one: ∂^0 is the identity and every other Hasse derivative kills constants.
• MvPolynomial.hasseDeriv_map, MvPolynomial.hasseDeriv_rename: Hasse derivatives commute with coefficient ring maps and with injective variable renamings.
• MvPolynomial.hasseDeriv_eq_zero_of_degreeOf_lt, MvPolynomial.degreeOf_hasseDeriv_le: the derivative lowers the degree in Xᵢ by dᵢ; in particular MvPolynomial.degreeOf_hasseDeriv_le_of_le keeps any bound degreeOf i P ≤ L i.
• MvPolynomial.factorial_smul_hasseDeriv_single: k! • ∂^(k eᵢ) P = (∂/∂Xᵢ)^k P.
• MvPolynomial.hasseDeriv_single_toMvPolynomial, MvPolynomial.hasseDeriv_toMvPolynomial_eq_zero: on a polynomial in the single variable Xᵢ, ∂^(k eᵢ) is the univariate k-th Hasse derivative, and ∂^d vanishes whenever d differentiates in another variable Xⱼ.
• MvPolynomial.hasseDeriv_comp: ∂^a ∘ ∂^b = (∏ⱼ (aⱼ + bⱼ choose aⱼ)) • ∂^(a + b).
• MvPolynomial.hasseDeriv_X, MvPolynomial.hasseDeriv_mul_X: the value on a variable and the Leibniz rule ∂^d (P Xᵢ) = ∂^(d - eᵢ) P + (∂^d P) Xᵢ (the first term only when dᵢ ≠ 0).

References

• L. Pottmeyer, Diophantine Approximation, lecture notes (2022), §2.6, Lemma 2.6.1 and §3.5.3.
• J.-H. Evertse, Diophantine Approximation, lecture notes (2019), ch. 6, p. 117.
• Mathlib's univariate Hasse derivative Polynomial.hasseDeriv (Mathlib/Algebra/Polynomial/HasseDeriv.lean, Johan Commelin), whose definition by lsum over monomials and whose statements of hasseDeriv_map and hasseDeriv_comp this file follows.

noncomputable def MvPolynomial.hasseDeriv {R : Type u_1} {σ : Type u_2} [CommSemiring R] (d : σ →₀ ℕ) : MvPolynomial σ R →ₗ[R] MvPolynomial σ R

The d-th Hasse derivative ∂^d of a multivariate polynomial, the linear map sending the monomial a X^m to (∏ⱼ (mⱼ choose dⱼ)) a X^(m - d). The coefficient vanishes unless d ≤ m.

@[simp]

theorem MvPolynomial.hasseDeriv_monomial {R : Type u_1} {σ : Type u_2} [CommSemiring 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) = (∏ⱼ (mⱼ choose dⱼ)) a X^(m - d).

theorem MvPolynomial.eval_const_hasseDeriv_monomial {R : Type u_1} {σ : Type u_2} [CommSemiring R] [Fintype σ] (x : R) (d m : σ →₀ ℕ) (a : R) : (eval fun (x_1 : σ) => x) ((hasseDeriv d) ((monomial m) a)) = ↑(∏ j : σ, (m j).choose (d j)) * (a * x ^ ∑ j : σ, (m j - d j))

The jet ∂^d (a X^m) at the diagonal point (x, …, x) is (∏ⱼ (mⱼ choose dⱼ)) a x ^ (∑ⱼ (mⱼ - dⱼ)).

@[simp]

theorem MvPolynomial.hasseDeriv_coeff {R : Type u_1} {σ : Type u_2} [CommSemiring R] (d m : σ →₀ ℕ) (P : MvPolynomial σ R) : ((hasseDeriv d) P).coeff m = ↑(d.prod fun (j : σ) (k : ℕ) => (m j + k).choose k) * P.coeff (m + d)

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

theorem MvPolynomial.abv_coeff_hasseDeriv_le {R : Type u_1} {σ : Type u_2} [CommSemiring R] {S : Type u_3} [Semiring S] [PartialOrder S] [IsOrderedRing S] (abv : AbsoluteValue R S) (d m : σ →₀ ℕ) (P : MvPolynomial σ R) : abv (((hasseDeriv d) P).coeff m) ≤ 2 ^ Finsupp.degree (m + d) * abv (P.coeff (m + d))

An absolute value of a coefficient of a Hasse derivative is at most 2 ^ |m + d| times that of the coefficient it comes from: v([X^m] ∂^d P) ≤ 2 ^ |m + d| v([X^(m + d)] P).

theorem MvPolynomial.abv_coeff_hasseDeriv_le_of_degreeOf_le {R : Type u_1} {σ : Type u_2} [CommSemiring R] {S : Type u_3} [Semiring S] [PartialOrder S] [IsOrderedRing S] [Fintype σ] (abv : AbsoluteValue R S) {P : MvPolynomial σ R} {r : σ → ℕ} (hdeg : ∀ (i : σ), degreeOf i P ≤ r i) (d m : σ →₀ ℕ) : abv (((hasseDeriv d) P).coeff m) ≤ (2 ^ ∑ i : σ, r i) * abv (P.coeff (m + d))

If P has partial degrees degreeOf i P ≤ r i, then v([X^m] ∂^d P) ≤ 2 ^ ∑ᵢ rᵢ * v([X^(m + d)] P).

theorem MvPolynomial.abv_coeff_hasseDeriv_le_two_pow_mul {R : Type u_1} {σ : Type u_2} [CommSemiring R] {S : Type u_3} [Semiring S] [PartialOrder S] [IsOrderedRing S] [Fintype σ] (abv : AbsoluteValue R S) {P : MvPolynomial σ R} {r : σ → ℕ} (hdeg : ∀ (i : σ), degreeOf i P ≤ r i) {B : S} (hB : ∀ (μ : σ →₀ ℕ), abv (P.coeff μ) ≤ B) (d m : σ →₀ ℕ) : abv (((hasseDeriv d) P).coeff m) ≤ (2 ^ ∑ i : σ, r i) * B

If P has partial degrees degreeOf i P ≤ r i and coefficients of absolute value at most B, then every coefficient of every Hasse derivative of P has absolute value at most 2 ^ ∑ᵢ rᵢ * B.

theorem MvPolynomial.abv_coeff_hasseDeriv_le_of_isNonarchimedean {R : Type u_1} {σ : Type u_2} [CommSemiring R] {S : Type u_3} [Semiring S] [LinearOrder S] {abv : AbsoluteValue R S} (hv : IsNonarchimedean ⇑abv) (d m : σ →₀ ℕ) (P : MvPolynomial σ R) : abv (((hasseDeriv d) P).coeff m) ≤ abv (P.coeff (m + d))

At a nonarchimedean absolute value the binomial coefficients of a Hasse derivative are at most 1, so v([X^m] ∂^d P) ≤ v([X^(m + d)] P).

@[simp]

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

The 0-th Hasse derivative is the identity.

@[simp]

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

Every Hasse derivative of positive order kills constants.

@[simp]

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

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

@[simp]

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

Hasse derivatives commute with coefficient ring maps.

theorem MvPolynomial.hasseDeriv_rename {R : Type u_1} {σ : Type u_2} [CommSemiring R] {τ : Type u_3} {f : σ → τ} (hf : Function.Injective f) (d : σ →₀ ℕ) (P : MvPolynomial σ R) : (hasseDeriv (Finsupp.mapDomain f d)) ((rename f) P) = (rename f) ((hasseDeriv d) P)

Hasse derivatives commute with injective variable renamings, with the derivative multi-index pushed forward along the renaming.

theorem MvPolynomial.hasseDeriv_eq_zero_of_degreeOf_lt {R : Type u_1} {σ : Type u_2} [CommSemiring R] {d : σ →₀ ℕ} {P : MvPolynomial σ R} {i : σ} (h : degreeOf i P < d i) : (hasseDeriv d) P = 0

If the degree of P in Xᵢ is less than dᵢ, then ∂^d P = 0.

theorem MvPolynomial.degreeOf_hasseDeriv_le {R : Type u_1} {σ : Type u_2} [CommSemiring R] (d : σ →₀ ℕ) (P : MvPolynomial σ R) (i : σ) : degreeOf i ((hasseDeriv d) P) ≤ degreeOf i P - d i

The Hasse derivative ∂^d lowers the degree in Xᵢ by at least dᵢ.

theorem MvPolynomial.degreeOf_hasseDeriv_le_of_le {R : Type u_1} {σ : Type u_2} [CommSemiring R] {P : MvPolynomial σ R} {L : σ → ℕ} (hL : ∀ (i : σ), degreeOf i P ≤ L i) (d : σ →₀ ℕ) (i : σ) : degreeOf i ((hasseDeriv d) P) ≤ L i

If P has partial degrees degreeOf i P ≤ L i, then so does every Hasse derivative of P.

@[simp]

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

Differentiating ∂^(k eᵢ) with respect to Xᵢ gives (k + 1) ∂^((k + 1) eᵢ).

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

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

@[simp]

theorem MvPolynomial.hasseDeriv_single_toMvPolynomial {R : Type u_1} {σ : Type u_2} [CommSemiring R] (i : σ) (k : ℕ) (p : Polynomial R) : (hasseDeriv (Finsupp.single i k)) ((Polynomial.toMvPolynomial i) p) = (Polynomial.toMvPolynomial i) ((Polynomial.hasseDeriv k) p)

On a polynomial in the single variable Xᵢ, the Hasse derivative ∂^(k eᵢ) is the univariate k-th Hasse derivative.

theorem MvPolynomial.hasseDeriv_toMvPolynomial_eq_zero {R : Type u_1} {σ : Type u_2} [CommSemiring R] {d : σ →₀ ℕ} {i j : σ} (hij : i ≠ j) (hd : d j ≠ 0) (p : Polynomial R) : (hasseDeriv d) ((Polynomial.toMvPolynomial i) p) = 0

On a polynomial in the single variable Xᵢ, every Hasse derivative ∂^d that differentiates in another variable Xⱼ (that is, dⱼ ≠ 0 for some j ≠ i) vanishes.

theorem MvPolynomial.hasseDeriv_comp {R : Type u_1} {σ : Type u_2} [CommSemiring 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 MvPolynomial.hasseDeriv_mul_X {R : Type u_1} {σ : Type u_2} [CommSemiring R] (d : σ →₀ ℕ) (P : MvPolynomial σ R) (i : σ) : (hasseDeriv d) (P * X i) = (if d i = 0 then 0 else (hasseDeriv (d - Finsupp.single i 1)) P) + (hasseDeriv d) P * X i

The Leibniz rule for multiplication by a variable: ∂^d (P Xᵢ) = ∂^(d - eᵢ) P + (∂^d P) Xᵢ, where the first term is present only when dᵢ ≠ 0.

@[simp]

theorem MvPolynomial.hasseDeriv_X {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq σ] (d : σ →₀ ℕ) (i : σ) : (hasseDeriv d) (X i) = if d = 0 then X i else if d = Finsupp.single i 1 then 1 else 0

The Hasse derivative of a variable is the variable in order zero, 1 in its corresponding first order, and 0 in every other order.