Hasse derivatives of restricted power series

Over an ultrametric (semi)normed ring, a natural-number multiple of an element has at most the norm of that element. The coefficients of the Hasse derivative D⁽ᵏ⁾ f are natural-number multiples of the coefficients of f, shifted down by k, so at a radius c > 0

‖D⁽ᵏ⁾ f‖_c ≤ c⁻ᵏ ‖f‖_c

for the Gauss norms, and D⁽ᵏ⁾ preserves restrictedness at every radius. Neither a multiplicative norm nor ‖1‖ = 1 is needed, and the coefficients need not commute. These are the estimates that make Hasse derivatives act on Tate algebras of closed discs of any positive radius.

Without the ultrametric hypothesis the binomial coefficients can grow, but only polynomially, so Hasse derivatives still carry restrictedness at one radius to restrictedness at every strictly smaller radius. This is what makes them act on series converging on open discs.

Main results

• PowerSeries.norm_coeff_hasseDeriv_le: ‖coeff n (D⁽ᵏ⁾ f)‖ ≤ ‖coeff (n + k) f‖.
• PowerSeries.IsRestricted.hasseDeriv: Hasse derivatives preserve restrictedness.
• PowerSeries.IsRestricted.hasseDeriv_of_abs_lt: over any normed ring, Hasse derivatives carry restrictedness at c' to restrictedness at every c with |c| < |c'|.
• PowerSeries.HasGaussNorm.hasseDeriv and PowerSeries.gaussNorm_hasseDeriv_le: at a positive radius c, Hasse derivatives preserve bounded weighted coefficients, and gaussNorm c (D⁽ᵏ⁾ f) ≤ c⁻¹ ^ k * gaussNorm c f.

References

• Bosch, Güntzer, Remmert, Non-Archimedean Analysis, §5.1.

theorem PowerSeries.norm_coeff_hasseDeriv_le {R : Type u_1} [SeminormedRing R] [IsUltrametricDist R] (f : PowerSeries R) (k n : ℕ) : ‖(coeff n) ((hasseDeriv k) f)‖ ≤ ‖(coeff (n + k)) f‖

Over an ultrametric ring, a coefficient of a Hasse derivative has at most the norm of the coefficient of f it is a multiple of.

theorem PowerSeries.norm_coeff_hasseDeriv_mul_pow_le {R : Type u_1} [SeminormedRing R] [IsUltrametricDist R] {c : ℝ} (f : PowerSeries R) (hc : 0 < c) (k n : ℕ) : ‖(coeff n) ((hasseDeriv k) f)‖ * c ^ n ≤ c⁻¹ ^ k * (‖(coeff (n + k)) f‖ * c ^ (n + k))

The weighted coefficient norms of D⁽ᵏ⁾ f at a positive radius c are bounded by c⁻ᵏ times those of f.

theorem PowerSeries.norm_coeff_hasseDeriv_mul_pow_le_gaussNorm {R : Type u_1} [SeminormedRing R] [IsUltrametricDist R] {c : ℝ} {f : PowerSeries R} (hc : 0 < c) (hf : HasGaussNorm norm c f) (k n : ℕ) : ‖(coeff n) ((hasseDeriv k) f)‖ * c ^ n ≤ c⁻¹ ^ k * gaussNorm norm c f

At a positive radius c, the weighted coefficient norms of D⁽ᵏ⁾ f are bounded by c⁻ᵏ times the Gauss norm of f, whenever f has bounded weighted coefficient norms.

theorem PowerSeries.HasGaussNorm.hasseDeriv {R : Type u_1} [SeminormedRing R] [IsUltrametricDist R] {c : ℝ} {f : PowerSeries R} (hc : 0 < c) (hf : HasGaussNorm norm c f) (k : ℕ) : HasGaussNorm norm c ((PowerSeries.hasseDeriv k) f)

At a positive radius, Hasse derivatives preserve boundedness of the weighted coefficient norms.

theorem PowerSeries.gaussNorm_hasseDeriv_le {R : Type u_1} [SeminormedRing R] [IsUltrametricDist R] {c : ℝ} {f : PowerSeries R} (hc : 0 < c) (hf : HasGaussNorm norm c f) (k : ℕ) : gaussNorm norm c ((hasseDeriv k) f) ≤ c⁻¹ ^ k * gaussNorm norm c f

The Gauss-norm estimate for Hasse derivatives: at a radius c > 0, ‖D⁽ᵏ⁾ f‖_c ≤ c⁻ᵏ ‖f‖_c whenever f has bounded weighted coefficient norms.

theorem PowerSeries.IsRestricted.hasseDeriv_of_abs_lt {R : Type u_1} [NormedRing R] {c c' : ℝ} {f : PowerSeries R} (hf : IsRestricted c' f) (h : |c| < |c'|) (k : ℕ) : IsRestricted c ((PowerSeries.hasseDeriv k) f)

Hasse derivatives at a smaller radius. Over any normed ring, if f is restricted at the radius c', then D⁽ᵏ⁾ f is restricted at every radius c with |c| < |c'|: the polynomial growth of the binomial coefficients is absorbed by the geometric factor (|c| / |c'|)ⁿ. Over an ultrametric ring no radius is lost (PowerSeries.IsRestricted.hasseDeriv).

theorem PowerSeries.IsRestricted.hasseDeriv {R : Type u_1} [NormedRing R] {c : ℝ} {f : PowerSeries R} [IsUltrametricDist R] (hf : IsRestricted c f) (k : ℕ) : IsRestricted c ((PowerSeries.hasseDeriv k) f)

Over an ultrametric normed ring, Hasse derivatives preserve restrictedness at every radius.