Values of Hasse derivatives of restricted power series

Over a complete ultrametric normed commutative ring R, a series q restricted at a radius c and all its Hasse derivatives D⁽ᵗ⁾ q can be evaluated at every point b with ‖b‖ ≤ c of a complete ultrametric normed R-algebra, and evaluation is a ring homomorphism on restricted series. Evaluating the formal Leibniz rule PowerSeries.hasseDeriv_succ_X_sub_C_mul therefore gives

(D⁽ᵗ⁺¹⁾ ((X - a) * q))(b) = (b - a) * (D⁽ᵗ⁺¹⁾ q)(b) + (D⁽ᵗ⁾ q)(b).

This is how vanishing conditions on the Hasse derivatives of (X - a) * q pass to q, as in the Schwarz lemma PowerSeries.IsRestricted.norm_evalAt_le_gaussNorm_mul_prod. Evaluating the composition rule D⁽ᵗ⁾ ∘ D⁽ᵏ⁾ = (t + k).choose t • D⁽ᵗ⁺ᵏ⁾ likewise shows that D⁽ᵏ⁾ q vanishes to order T - k wherever q vanishes to order T.

The values of Hasse derivatives are also controlled by the coefficients of q: if ε ≥ 0 bounds the weighted coefficient norms ‖qₖ‖ cᵏ in every degree k ≥ n, then ‖(D⁽ⁿ⁾ q)(a)‖ cⁿ ≤ ε at every a with ‖a‖ ≤ c. This needs neither completeness nor ‖1‖ = 1.

Main results

• PowerSeries.norm_evalAt_hasseDeriv_mul_pow_le_of_forall: a bound on the weighted coefficients of q in degrees ≥ n bounds ‖(D⁽ⁿ⁾ q)(a)‖ cⁿ.
• PowerSeries.IsRestricted.evalAt_hasseDeriv_succ_X_sub_C_mul: the evaluated Leibniz rule for (X - a) * q.
• PowerSeries.IsRestricted.evalAt_hasseDeriv_hasseDeriv: the evaluated composition rule (D⁽ᵗ⁾ (D⁽ᵏ⁾ q))(b) = (t + k).choose t • (D⁽ᵗ⁺ᵏ⁾ q)(b).

theorem PowerSeries.norm_evalAt_hasseDeriv_mul_pow_le_of_forall {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] {c : ℝ} {q : PowerSeries R} {a : R} (hc : 0 < c) (ha : ‖a‖ ≤ c) {ε : ℝ} (n : ℕ) (h : ∀ (m : ℕ), ‖(coeff (m + n)) q‖ * c ^ (m + n) ≤ ε) : ‖((hasseDeriv n) q).evalAt a‖ * c ^ n ≤ ε

If ε bounds the weighted coefficient norms ‖qₖ‖ cᵏ of q in every degree k ≥ n, then it bounds ‖(D⁽ⁿ⁾ q)(a)‖ cⁿ at every point a with ‖a‖ ≤ c.

theorem PowerSeries.IsRestricted.evalAt_hasseDeriv_succ_X_sub_C_mul {R : Type u_1} {A : Type u_2} [NormedCommRing R] [IsUltrametricDist R] [NormedRing A] [Algebra R A] [IsBoundedSMul R A] [IsUltrametricDist A] [CompleteSpace A] {c : ℝ} {q : PowerSeries R} (hq : IsRestricted c q) (a : R) {b : A} (hb : ‖b‖ ≤ c) (t : ℕ) : ((PowerSeries.hasseDeriv (t + 1)) ((X - C a) * q)).evalAt b = (b - (algebraMap R A) a) * ((PowerSeries.hasseDeriv (t + 1)) q).evalAt b + ((PowerSeries.hasseDeriv t) q).evalAt b

Evaluated Leibniz rule for (X - a) * q. At a point b with ‖b‖ ≤ c, the Hasse derivative of order t + 1 of (X - a) * q, for q restricted at c, takes the value (b - a) * (D⁽ᵗ⁺¹⁾ q)(b) + (D⁽ᵗ⁾ q)(b).

theorem PowerSeries.IsRestricted.evalAt_hasseDeriv_hasseDeriv {R : Type u_1} {A : Type u_2} [NormedCommRing R] [IsUltrametricDist R] [NormedRing A] [Algebra R A] [IsBoundedSMul R A] [IsUltrametricDist A] [CompleteSpace A] {c : ℝ} {q : PowerSeries R} (hq : IsRestricted c q) {b : A} (hb : ‖b‖ ≤ c) (t k : ℕ) : ((PowerSeries.hasseDeriv t) ((PowerSeries.hasseDeriv k) q)).evalAt b = (t + k).choose t • ((PowerSeries.hasseDeriv (t + k)) q).evalAt b

Evaluated composition of Hasse derivatives. At a point b with ‖b‖ ≤ c, for q restricted at c, (D⁽ᵗ⁾ (D⁽ᵏ⁾ q))(b) = (t + k).choose t • (D⁽ᵗ⁺ᵏ⁾ q)(b). In particular, if q vanishes at b to order T, then D⁽ᵏ⁾ q vanishes at b to order T - k.