Mv Power Series

Results named in Tau Ceti's TauCeti.RingTheory.MvPowerSeries modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremThe Cauchy estimate for partial derivatives#

‖∂ᵢ f‖ ≤ cᵢ⁻¹ ‖f‖ for the Gauss norm at the polyradius c.

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

Formalized in Tau Ceti as TauCeti.MvPowerSeries.norm_restrictedPDeriv_le.

Other forms

The Cauchy estimate on the restricted-series ring. Formalized in Tau Ceti as MvPowerSeries.norm_restrictedHasseDeriv_le.

MvPowerSeries.norm_restrictedHasseDeriv_le.{u_1, u_2} {σ : Type u_1} {R : Type u_2} [NormedRing R]
  [IsUltrametricDist R] {c : σ → ℝ} [∀ (i : σ), Fact (0 < c i)] (d : σ →₀ ℕ)
  (f : ↥(MvPowerSeries.IsRestricted.subring c)) :
  ‖(MvPowerSeries.restrictedHasseDeriv d) f‖ ≤ (d.prod fun x1 x2 => c x1 ^ x2)⁻¹ * ‖f‖
Sources
LeanTauCeti.MvPowerSeries.norm_restrictedPDeriv_le · MvPowerSeries.norm_restrictedHasseDeriv_le
Used by 1
Used byThe Cauchy estimate at unit radius

TheoremKedlaya's Hilbert basis theorem for restricted power series#

Kedlaya's Hilbert basis theorem for restricted power series, the argument of Kedlaya's Theorem 3.2 for an abstract Euclidean normed ring. Let R be a complete ring with a multiplicative ultrametric norm, and deg : R → ℕ a degree such that deg y = deg x whenever ‖x - y‖ < ‖x‖, and such that for x ≠ 0 every y can be divided as y = z * x + w with ‖w‖ ≤ ‖y‖ and either w = 0 or deg w < deg x. Then for finitely many variables and all positive radii c, the ring of restricted power series with its Gauss norm at the radii c is left noetherian.

TauCeti.MvPowerSeries.isNoetherianRing_isRestricted_subring_of_division.{u_1, u_2} {σ : Type u_1}
  {R : Type u_2} [NormedRing R] [IsUltrametricDist R] {c : σ → ℝ} [∀ (i : σ), Fact (0 < c i)]
  [NormMulClass R] [CompleteSpace R] [Finite σ] (deg : R → ℕ)
  (hdeg : ∀ (x y : R), ‖x - y‖ < ‖x‖ → deg y = deg x)
  (hdiv : ∀ (x y : R), x ≠ 0 → ∃ z w, y = z * x + w ∧ ‖w‖ ≤ ‖y‖ ∧ (w = 0 ∨ deg w < deg x)) :
  IsNoetherianRing ↥(MvPowerSeries.IsRestricted.subring c)
Lean

Formalized in Tau Ceti as TauCeti.MvPowerSeries.isNoetherianRing_isRestricted_subring_of_division.

Other forms

Kedlaya's Hilbert basis theorem for A^r (Kedlaya, Theorem 3.2). Formalized in Tau Ceti as TauCeti.WittVector.RadiusRing.isNoetherianRing_isRestricted_subring.

TauCeti.WittVector.RadiusRing.isNoetherianRing_isRestricted_subring.{u_1, u_2, u_3} (p : ℕ)
  [Fact (Nat.Prime p)] {K : Type u_1} {O : Type u_2} [Field K] [CommRing O] [Algebra O K]
  {v : Valuation K NNReal} {ϖ : O} [CharP O p] [PerfectRing O p] (hv : v.Integers O) (hϖ : ϖ ≠ 0)
  (hϖ' : v ((algebraMap O K) ϖ) < 1) {ρ : NNReal} (hρ : ρ ∈ Set.Ioo 0 1) {σ : Type u_3} [Finite σ]
  {c : σ → ℝ} [∀ (i : σ), Fact (0 < c i)] : IsNoetherianRing ↥(MvPowerSeries.IsRestricted.subring c)
Sources
LeanTauCeti.MvPowerSeries.isNoetherianRing_isRestricted_subring_of_division · TauCeti.WittVector.RadiusRing.isNoetherianRing_isRestricted_subring
Used by 12
Used byTate's acyclicity theorem for the standard Laurent cover of the closed unit disc · Affinoid algebras are the algebras topologically of finite type · The adic spectrum of a classical affinoid algebra is an affinoid adic space · The interval ring B^I is strongly noetherian · Equivalence of complete affinoid norms · Heights of maximal ideals of affinoid domains · Restricted series over an affinoid algebra form an affinoid algebra · TauCeti.IsAffinoidAlgebra.continuous_algHom · TauCeti.MvPowerSeries.supSeminorm_eq_norm · The maximum modulus principle · The supremum seminorm is the spectral value of the minimal polynomial · The universal property of restricted series over an affinoid algebra

TheoremNeumann series criterion (MvPowerSeries.isNormMulUnit_of_norm_sub_C_lt)#

Over a complete ultrametric norm-one ring, a restricted series whose distance from a constant multiplicative unit a is less than ‖a‖ is a multiplicative unit.

MvPowerSeries.isNormMulUnit_of_norm_sub_C_lt.{u_1, u_2} {σ : Type u_1} {R : Type u_2} [NormedRing R]
  [IsUltrametricDist R] {c : σ → ℝ} [∀ (i : σ), Fact (0 < c i)] [NormOneClass R] [CompleteSpace R]
  {a : R} (ha : TauCeti.IsNormMulUnit a) {f : ↥(MvPowerSeries.IsRestricted.subring c)}
  (hf : ‖f - ⟨MvPowerSeries.C a, ⋯⟩‖ < ‖a‖) : TauCeti.IsNormMulUnit f
Lean

Formalized in Tau Ceti as MvPowerSeries.isNormMulUnit_of_norm_sub_C_lt.

Sources
LeanMvPowerSeries.isNormMulUnit_of_norm_sub_C_lt
Uses 1 · Used by 2
Proof usesNeumann series criterion (TauCeti.IsNormMulUnit.of_norm_sub_lt)
Used byRadius selection for distinguished overconvergent series · Units of the Monsky–Washnitzer algebra

TheoremThe Weierstrass division estimate in several variables#

Over an ultrametric normed commutative ring, let the iterated series of g in the separated variable X none be multiplicatively distinguished of degree s. If r has degree less than s in X none, then

‖g * q + r‖ = max (‖g‖ * ‖q‖) ‖r‖

for the Gauss norms at the polyradii c. The norm of the coefficient ring need not be multiplicative.

TauCeti.MvPowerSeries.norm_mul_add_eq_max_of_isMulDistinguished.{u_1, u_2} {σ : Type u_1}
  {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] {c : Option σ → ℝ}
  [∀ (i : Option σ), Fact (0 < c i)] {s : ℕ} {g : ↥(MvPowerSeries.IsRestricted.subring c)}
  (hg : TauCeti.PowerSeries.IsMulDistinguished (c none) s ↑(MvPowerSeries.restrictedOptionEquiv g))
  (q : ↥(MvPowerSeries.IsRestricted.subring c)) {r : ↥(MvPowerSeries.IsRestricted.subring c)}
  (hr : ∀ (t : Option σ →₀ ℕ), s ≤ t none → (MvPowerSeries.coeff t) ↑r = 0) :
  ‖g * q + r‖ = max (‖g‖ * ‖q‖) ‖r‖
Lean

Formalized in Tau Ceti as TauCeti.MvPowerSeries.norm_mul_add_eq_max_of_isMulDistinguished.

Sources
LeanTauCeti.MvPowerSeries.norm_mul_add_eq_max_of_isMulDistinguished
Uses 1
Proof usesThe Weierstrass division estimate (Bosch–Güntzer–Remmert §5.2.1, Theorem 2)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.