Partial derivatives of restricted power series and the chain rule

Let R be an ultrametric normed commutative ring and c a positive polyradius. The partial derivative ∂/∂Xᵢ of Mathlib's MvPowerSeries.pderiv preserves restrictedness at c, so it is an R-derivation of the restricted-series ring R{X/c}. It is the first Hasse derivative in Xᵢ, and satisfies the Cauchy estimate ‖∂ᵢ f‖ ≤ cᵢ⁻¹ ‖f‖; in particular it is continuous for the Gauss norm.

Over a complete coefficient ring, partial derivatives obey the chain rule for analytic substitution: for series gᵢ ∈ R{Y/s} with ‖gᵢ‖ ≤ rᵢ and f ∈ R{X/r},

∂ⱼ (f(g)) = ∑ᵢ (∂ᵢ f)(g) · ∂ⱼ gᵢ.

Unlike the formal chain rule MvPowerSeries.pderiv_subst, the gᵢ may have arbitrary, even non-nilpotent, constant terms: the substitution is the convergent sum TauCeti.MvPowerSeries.restrictedAnalyticSubst. In particular, translation Xᵢ ↦ Xᵢ + aᵢ of a closed polydisc commutes with every partial derivative.

Main definitions

• TauCeti.MvPowerSeries.restrictedPDeriv: the partial derivative ∂/∂Xᵢ as an R-derivation of R{X/c}.

Main results

• TauCeti.MvPowerSeries.restrictedHasseDeriv_single_one: the first Hasse derivative in Xᵢ is the partial derivative.
• TauCeti.MvPowerSeries.norm_restrictedPDeriv_le: the Cauchy estimate ‖∂ᵢ f‖ ≤ cᵢ⁻¹ ‖f‖.
• TauCeti.MvPowerSeries.restrictedPDeriv_restrictedAnalyticSubst: the chain rule for analytic substitution.
• TauCeti.MvPowerSeries.restrictedPDeriv_restrictedTranslate: partial derivatives commute with translation.

References

• S. Bosch, U. Güntzer and R. Remmert, Non-Archimedean Analysis, Grundlehren 261, §5.1.

noncomputable def TauCeti.MvPowerSeries.restrictedPDeriv {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] {c : σ → ℝ} [∀ (i : σ), Fact (0 < c i)] (i : σ) : Derivation R ↥(MvPowerSeries.IsRestricted.subring c) ↥(MvPowerSeries.IsRestricted.subring c)

The partial derivative ∂/∂Xᵢ, as an R-derivation of the ring R{X/c} of series restricted at a positive polyradius c.

@[simp]

theorem TauCeti.MvPowerSeries.coe_restrictedPDeriv {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] {c : σ → ℝ} [∀ (i : σ), Fact (0 < c i)] (i : σ) (f : ↥(MvPowerSeries.IsRestricted.subring c)) : ↑((restrictedPDeriv i) f) = (MvPowerSeries.pderiv i) ↑f

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

@[simp]

theorem TauCeti.MvPowerSeries.restrictedHasseDeriv_single_one {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] {c : σ → ℝ} [∀ (i : σ), Fact (0 < c i)] (i : σ) (f : ↥(MvPowerSeries.IsRestricted.subring c)) : (MvPowerSeries.restrictedHasseDeriv (Finsupp.single i 1)) f = (restrictedPDeriv i) f

The first Hasse derivative in Xᵢ is the partial derivative in Xᵢ.

@[simp]

theorem TauCeti.MvPowerSeries.restrictedPDeriv_X_self {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] {c : σ → ℝ} [∀ (i : σ), Fact (0 < c i)] (i : σ) : (restrictedPDeriv i) ⟨MvPowerSeries.X i, ⋯⟩ = 1

The partial derivative of Xᵢ in Xᵢ is 1.

@[simp]

theorem TauCeti.MvPowerSeries.restrictedPDeriv_X_of_ne {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] {c : σ → ℝ} [∀ (i : σ), Fact (0 < c i)] {i j : σ} (h : j ≠ i) : (restrictedPDeriv i) ⟨MvPowerSeries.X j, ⋯⟩ = 0

The partial derivative of Xⱼ in Xᵢ is 0 for j ≠ i.

theorem TauCeti.MvPowerSeries.restrictedPDeriv_X {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] {c : σ → ℝ} [∀ (i : σ), Fact (0 < c i)] [DecidableEq σ] (i j : σ) : (restrictedPDeriv i) ⟨MvPowerSeries.X j, ⋯⟩ = Pi.single i 1 j

The partial derivatives of the variables: ∂Xⱼ/∂Xᵢ = δᵢⱼ.

theorem TauCeti.MvPowerSeries.norm_restrictedPDeriv_le {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] {c : σ → ℝ} [∀ (i : σ), Fact (0 < c i)] (i : σ) (f : ↥(MvPowerSeries.IsRestricted.subring c)) : ‖(restrictedPDeriv i) f‖ ≤ (c i)⁻¹ * ‖f‖

The Cauchy estimate for partial derivatives: ‖∂ᵢ f‖ ≤ cᵢ⁻¹ ‖f‖ for the Gauss norm at the polyradius c.

theorem TauCeti.MvPowerSeries.continuous_restrictedPDeriv {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] {c : σ → ℝ} [∀ (i : σ), Fact (0 < c i)] (i : σ) : Continuous ⇑(restrictedPDeriv i)

Partial derivatives are continuous for the Gauss norm.

theorem TauCeti.MvPowerSeries.restrictedPDeriv_restrictedAnalyticSubst {k : ℕ} {τ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] [CompleteSpace R] {r : Fin k → ℝ} {s : τ → ℝ} [∀ (i : Fin k), Fact (0 < r i)] [∀ (j : τ), Fact (0 < s j)] (g : Fin k → ↥(MvPowerSeries.IsRestricted.subring s)) (hg : ∀ (i : Fin k), ‖g i‖ ≤ r i) (j : τ) (f : ↥(MvPowerSeries.IsRestricted.subring r)) : (restrictedPDeriv j) ((restrictedAnalyticSubst g hg) f) = ∑ i : Fin k, (restrictedAnalyticSubst g hg) ((restrictedPDeriv i) f) * (restrictedPDeriv j) (g i)

The chain rule for analytic substitution: for series gᵢ ∈ R{Y/s} with ‖gᵢ‖ ≤ rᵢ and f ∈ R{X/r}, ∂ⱼ (f(g)) = ∑ᵢ (∂ᵢ f)(g) · ∂ⱼ gᵢ. The gᵢ may have nonzero constant terms.

theorem TauCeti.MvPowerSeries.restrictedPDeriv_restrictedTranslate {k : ℕ} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] [CompleteSpace R] {r : Fin k → ℝ} [∀ (i : Fin k), Fact (0 < r i)] [NormOneClass R] (a : Fin k → R) (ha : ∀ (i : Fin k), ‖a i‖ ≤ r i) (i : Fin k) (f : ↥(MvPowerSeries.IsRestricted.subring r)) : (restrictedPDeriv i) ((restrictedTranslate a ha) f) = (restrictedTranslate a ha) ((restrictedPDeriv i) f)

Translation commutes with partial derivatives: ∂ᵢ (f(X + a)) = (∂ᵢ f)(X + a).