Hasse derivatives as Taylor coefficients

The Taylor coefficients of a multivariate polynomial are its Hasse derivatives: for the Taylor shift MvPolynomial.taylor a, [Y^d] P(a + Y) = (∂^d P)(a), so that P(a + y) = ∑_d (∂^d P)(a) y^d. Comparing Taylor coefficients of a product gives the Leibniz rule for Hasse derivatives.

Main results

• MvPolynomial.coeff_taylor_X_map_C, MvPolynomial.coeff_taylor: the Taylor coefficients of P at the generic point and at a point a are the Hasse derivatives ∂^d P and their values (∂^d P)(a).
• MvPolynomial.eval_add_eq_finsum_hasseDeriv: the finite Taylor expansion P(a + y) = ∑_d (∂^d P)(a) y^d.
• MvPolynomial.hasseDeriv_mul: the Leibniz rule ∂^d (P Q) = ∑_{a + b = d} ∂^a P · ∂^b Q.
• MvPolynomial.hasseDeriv_add_single_mul_toMvPolynomial: the Leibniz rule for a product f · p(Xᵢ) in separated variables, ∂^(d + l eᵢ) (f · p(Xᵢ)) = ∂^d f · (Dˡ p)(Xᵢ) when neither f nor d involves Xᵢ.

References

• L. Pottmeyer, Diophantine Approximation, lecture notes (2022), §2.6, Lemma 2.6.1.
• Mathlib's univariate Polynomial.taylor_coeff (Mathlib/Algebra/Polynomial/Taylor.lean), the one-variable form of MvPolynomial.coeff_taylor.

theorem MvPolynomial.coeff_taylor_X_map_C {R : Type u_1} {σ : Type u_2} [CommSemiring R] (d : σ →₀ ℕ) (P : MvPolynomial σ R) : ((taylor X) ((map C) P)).coeff d = (hasseDeriv d) P

The Taylor coefficients of P at the generic point are its Hasse derivatives: P(X + Y) = ∑_d (∂^d P)(X) Y^d.

theorem MvPolynomial.coeff_taylor {R : Type u_1} {σ : Type u_2} [CommSemiring R] (a : σ → R) (d : σ →₀ ℕ) (P : MvPolynomial σ R) : ((taylor a) P).coeff d = (eval a) ((hasseDeriv d) P)

The Taylor coefficients of P at the point a are the values of its Hasse derivatives: [Y^d] P(a + Y) = (∂^d P)(a).

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

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

theorem MvPolynomial.hasseDeriv_add_single_mul_toMvPolynomial {R : Type u_1} {σ : Type u_2} [CommSemiring R] {d : σ →₀ ℕ} {i : σ} (hd : d i = 0) {f : MvPolynomial σ R} (hf : i ∉ f.vars) (l : ℕ) (p : Polynomial R) : (hasseDeriv (d + Finsupp.single i l)) (f * (Polynomial.toMvPolynomial i) p) = (hasseDeriv d) f * (Polynomial.toMvPolynomial i) ((Polynomial.hasseDeriv l) p)

The Leibniz rule for a product in separated variables: if f does not involve Xᵢ and d does not differentiate in Xᵢ, then ∂^(d + l eᵢ) (f · p(Xᵢ)) = ∂^d f · (Dˡ p)(Xᵢ), where Dˡ is the one-variable Hasse derivative.

theorem MvPolynomial.eval_add_eq_finsum_hasseDeriv {R : Type u_1} {σ : Type u_2} [CommSemiring R] (P : MvPolynomial σ R) (a y : σ → R) : (eval (a + y)) P = ∑ᶠ (d : σ →₀ ℕ), (eval a) ((hasseDeriv d) P) * d.prod fun (j : σ) (k : ℕ) => y j ^ k

The finite Taylor expansion with Hasse derivatives: P(a + y) = ∑_d (∂^d P)(a) y^d.