Hasse derivatives of restricted multivariate 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 d, so for a polyradius c ≥ 0

cᵈ ‖∂^d f‖_c ≤ ‖f‖_c,    cᵈ = ∏ᵢ cᵢ ^ dᵢ,

for the Gauss norms, and ∂^d preserves restrictedness whenever cᵢ ≠ 0 in every variable Xᵢ in which it differentiates. 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 polydiscs of any positive polyradius.

The condition on the polyradius cannot be dropped: at c = (0, 1) in the variables X, Y, the series ∑ₙ X Yⁿ is restricted, since every weight involving X vanishes, but its derivative ∑ₙ Yⁿ in X is not.

Main results

• MvPowerSeries.norm_coeff_hasseDeriv_le: ‖[Xᵐ] ∂^d f‖ ≤ ‖[X^(m + d)] f‖.
• MvPowerSeries.prod_pow_mul_gaussNorm_hasseDeriv_le: cᵈ ‖∂^d f‖_c ≤ ‖f‖_c whenever f has bounded weighted coefficient norms.
• MvPowerSeries.HasGaussNorm.hasseDeriv and MvPowerSeries.IsRestricted.hasseDeriv: Hasse derivatives preserve bounded weighted coefficient norms and restrictedness.
• MvPowerSeries.IsRestricted.pderiv: over a commutative ring, the partial derivative in Xᵢ preserves restrictedness whenever cᵢ ≠ 0.
• MvPowerSeries.restrictedHasseDeriv: the Hasse derivative on the ring of series restricted at a positive polyradius c, with the Cauchy estimate MvPowerSeries.norm_restrictedHasseDeriv_le, ‖∂^d f‖ ≤ (∏ᵢ cᵢ ^ dᵢ)⁻¹ ‖f‖, its continuity, and over a commutative ring its R-linearity MvPowerSeries.restrictedHasseDeriv_smul and its agreement MvPowerSeries.restrictedHasseDeriv_polynomial with MvPolynomial.hasseDeriv.

References

• Bosch, Güntzer, Remmert, Non-Archimedean Analysis, §5.1.
• E. Grosse-Klönne, Rigid analytic spaces with overconvergent structure sheaf, J. reine angew. Math. 519 (2000), §1.2.

theorem MvPowerSeries.norm_coeff_hasseDeriv_le {σ : Type u_1} {R : Type u_2} [SeminormedRing R] [IsUltrametricDist R] (f : MvPowerSeries σ R) (d m : σ →₀ ℕ) : ‖(coeff m) ((hasseDeriv d) f)‖ ≤ ‖(coeff (m + d)) 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 MvPowerSeries.prod_pow_mul_norm_coeff_hasseDeriv_le {σ : Type u_1} {R : Type u_2} [SeminormedRing R] [IsUltrametricDist R] {c : σ → ℝ} (f : MvPowerSeries σ R) (hc : 0 ≤ c) (d m : σ →₀ ℕ) : (d.prod fun (x1 : σ) (x2 : ℕ) => c x1 ^ x2) * (‖(coeff m) ((hasseDeriv d) f)‖ * m.prod fun (x1 : σ) (x2 : ℕ) => c x1 ^ x2) ≤ ‖(coeff (m + d)) f‖ * (m + d).prod fun (x1 : σ) (x2 : ℕ) => c x1 ^ x2

For a polyradius c ≥ 0, the weighted coefficient norms of ∂^d f, multiplied by cᵈ, are bounded by those of f.

theorem MvPowerSeries.prod_pow_mul_gaussNorm_hasseDeriv_le {σ : Type u_1} {R : Type u_2} [SeminormedRing R] [IsUltrametricDist R] {c : σ → ℝ} {f : MvPowerSeries σ R} (hc : 0 ≤ c) (hf : HasGaussNorm norm c f) (d : σ →₀ ℕ) : (d.prod fun (x1 : σ) (x2 : ℕ) => c x1 ^ x2) * gaussNorm norm c ((hasseDeriv d) f) ≤ gaussNorm norm c f

The Gauss-norm estimate for Hasse derivatives: for a polyradius c ≥ 0, cᵈ ‖∂^d f‖_c ≤ ‖f‖_c whenever f has bounded weighted coefficient norms.

theorem MvPowerSeries.HasGaussNorm.hasseDeriv {σ : Type u_1} {R : Type u_2} [SeminormedRing R] [IsUltrametricDist R] {c : σ → ℝ} {f : MvPowerSeries σ R} (hc : 0 ≤ c) {d : σ →₀ ℕ} (hd : ∀ i ∈ d.support, c i ≠ 0) (hf : HasGaussNorm norm c f) : HasGaussNorm norm c ((MvPowerSeries.hasseDeriv d) f)

For a polyradius c ≥ 0 that is nonzero in every variable in which ∂^d differentiates, Hasse derivatives preserve boundedness of the weighted coefficient norms.

theorem MvPowerSeries.IsRestricted.hasseDeriv {σ : Type u_1} {R : Type u_2} [NormedRing R] [IsUltrametricDist R] {c : σ → ℝ} {f : MvPowerSeries σ R} {d : σ →₀ ℕ} (hd : ∀ i ∈ d.support, c i ≠ 0) (hf : IsRestricted c f) : IsRestricted c ((MvPowerSeries.hasseDeriv d) f)

Over an ultrametric normed ring, Hasse derivatives preserve restrictedness at every polyradius which is nonzero in each variable in which they differentiate.

noncomputable def MvPowerSeries.restrictedHasseDeriv {σ : Type u_1} {R : Type u_2} [NormedRing R] [IsUltrametricDist R] {c : σ → ℝ} [∀ (i : σ), Fact (0 < c i)] (d : σ →₀ ℕ) : ↥(IsRestricted.subring c) →+ ↥(IsRestricted.subring c)

The d-th Hasse derivative on the ring of series restricted at a positive polyradius c.

@[simp]

theorem MvPowerSeries.coe_restrictedHasseDeriv {σ : Type u_1} {R : Type u_2} [NormedRing R] [IsUltrametricDist R] {c : σ → ℝ} [∀ (i : σ), Fact (0 < c i)] (d : σ →₀ ℕ) (f : ↥(IsRestricted.subring c)) : ↑((restrictedHasseDeriv d) f) = (hasseDeriv d) ↑f

The Hasse derivative of a restricted series is its Hasse derivative as a formal series.

theorem MvPowerSeries.norm_restrictedHasseDeriv_le {σ : Type u_1} {R : Type u_2} [NormedRing R] [IsUltrametricDist R] {c : σ → ℝ} [∀ (i : σ), Fact (0 < c i)] (d : σ →₀ ℕ) (f : ↥(IsRestricted.subring c)) : ‖(restrictedHasseDeriv d) f‖ ≤ (d.prod fun (x1 : σ) (x2 : ℕ) => c x1 ^ x2)⁻¹ * ‖f‖

The Cauchy estimate on the restricted-series ring. At a positive polyradius c, ‖∂^d f‖ ≤ (∏ᵢ cᵢ ^ dᵢ)⁻¹ ‖f‖ for the Gauss norm.

theorem MvPowerSeries.lipschitzWith_restrictedHasseDeriv {σ : Type u_1} {R : Type u_2} [NormedRing R] [IsUltrametricDist R] {c : σ → ℝ} [∀ (i : σ), Fact (0 < c i)] (d : σ →₀ ℕ) : LipschitzWith (d.prod fun (x1 : σ) (x2 : ℕ) => c x1 ^ x2)⁻¹.toNNReal ⇑(restrictedHasseDeriv d)

The Hasse derivative on the restricted-series ring is Lipschitz with constant (∏ᵢ cᵢ ^ dᵢ)⁻¹.

theorem MvPowerSeries.continuous_restrictedHasseDeriv {σ : Type u_1} {R : Type u_2} [NormedRing R] [IsUltrametricDist R] {c : σ → ℝ} [∀ (i : σ), Fact (0 < c i)] (d : σ →₀ ℕ) : Continuous ⇑(restrictedHasseDeriv d)

The Hasse derivative on the restricted-series ring is continuous for the Gauss norm.

theorem MvPowerSeries.IsRestricted.pderiv {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] {c : σ → ℝ} {i : σ} (hi : c i ≠ 0) {f : MvPowerSeries σ R} (hf : IsRestricted c f) : IsRestricted c ((MvPowerSeries.pderiv i) f)

Over an ultrametric normed commutative ring, the partial derivative in Xᵢ preserves restrictedness at every polyradius with cᵢ ≠ 0.

@[simp]

theorem MvPowerSeries.restrictedHasseDeriv_smul {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] {c : σ → ℝ} [∀ (i : σ), Fact (0 < c i)] (d : σ →₀ ℕ) (r : R) (f : ↥(IsRestricted.subring c)) : (restrictedHasseDeriv d) (r • f) = r • (restrictedHasseDeriv d) f

Over a commutative ring, the Hasse derivative on the restricted-series ring is R-linear.

@[simp]

theorem MvPowerSeries.restrictedHasseDeriv_polynomial {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] {c : σ → ℝ} [∀ (i : σ), Fact (0 < c i)] (d : σ →₀ ℕ) (p : MvPolynomial σ R) : (restrictedHasseDeriv d) ⟨↑p, ⋯⟩ = ⟨↑((MvPolynomial.hasseDeriv d) p), ⋯⟩

On a polynomial, the Hasse derivative on the restricted-series ring is the polynomial Hasse derivative MvPolynomial.hasseDeriv.