Evaluating a weighted restricted power series

Wedhorn's universal property of A⟨X₁, …, Xₖ⟩_T (Proposition 5.50) sends a T-restricted series to the sum of its terms at a chosen tuple b. Before there is a map to speak of, that sum has to exist, and this file supplies exactly that: the family of terms is summable.

Summability is where the defining condition earns its keep. T-restrictedness says that for each open subgroup U of A, all but finitely many coefficients lie in Tν · U; so all but finitely many terms lie in (φ(Tν) · bν) · φ(U). If the weighted monomials φ(Tν) · bν stay inside one bounded set — TauCeti.Huber.IsWeightBounded below, which is Wedhorn's hypothesis that the variables are power-bounded relative to the weights — then shrinking U shrinks every one of those terms at once, so the terms tend to zero along the cofinite filter. That convergence is the necessary condition, not yet the sufficient one: it is completeness of the target that upgrades it to summability, through Mathlib's NonarchimedeanAddGroup.summable_of_tendsto_cofinite_zero.

Main definitions

• TauCeti.Huber.weightedEvalTerm: the term φ(coeff ν f) · bν of the evaluation.
• TauCeti.Huber.weightedVar and TauCeti.Huber.IsWeightedVarPowerBounded: Wedhorn's own coordinatewise hypothesis — each weighted variable φ(Tᵢ) · bᵢ is power-bounded as a set.
• TauCeti.Huber.IsWeightBounded: the weighted monomials φ(Tν) · bν form a bounded set. This is the hypothesis the summability proof uses, and TauCeti.Huber.isWeightBounded_of_isWeightedVarPowerBounded derives it from the coordinatewise one for an arbitrary T. At the one-weight family it is equivalent to each bᵢ being power-bounded, which is Wedhorn's condition — TauCeti.Huber.isWeightBounded_one_weight_iff_forall_isPowerBounded.

Main results

• TauCeti.Huber.tendsto_weightedEvalTerm_cofinite_zero: the terms tend to zero along the cofinite filter. This is the analytic input, and it needs no completeness.
• TauCeti.Huber.summable_weightedEvalTerm: completeness upgrades that convergence to summability.
• TauCeti.Huber.summable_weightedEvalTerm_of_isWeightedVarPowerBounded: the same stated with Wedhorn's coordinatewise hypothesis, for an arbitrary weight family.
• TauCeti.Huber.summable_weightedEvalTerm_of_forall_isPowerBounded: its one-weight reading, where the hypothesis is that each variable is power-bounded.

This file proves only the summability that the evaluation needs. The evaluation map itself is TauCeti.Huber.weightedEval in WeightedEval/Map.lean, its packaging as a ring homomorphism is TauCeti.Huber.weightedEvalHom in WeightedEval/Hom.lean, and its continuity is TauCeti.Huber.continuous_weightedEvalHom in WeightedEval/Continuous.lean. The uniqueness that makes Proposition 5.50 a universal property is TauCeti.Huber.weightedRestrictedSubring_ringHom_ext_of_continuous in WeightedRestrictedSeries/Basic.lean. WeightedEval/UniversalProperty.lean assembles the two into an ∃!, and states Proposition 5.50 itself — under Wedhorn's own coordinatewise hypothesis — as existsUnique_continuous_ringHom_weightedRestrictedSubring_of_isWeightedVarPowerBounded.

References

• Wedhorn, Adic Spaces, Proposition 5.50, whose analytic core this is.

def TauCeti.Huber.weightedEvalTerm {k : ℕ} {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (φ : A →+* B) (b : Fin k → B) (f : MvPowerSeries (Fin k) A) (ν : Fin k →₀ ℕ) : B

The ν-th term of the evaluation of f at b along φ, namely φ(coeff ν f) · bν.

Equations

• TauCeti.Huber.weightedEvalTerm φ b f ν = φ ((MvPowerSeries.coeff ν) f) * ∏ i : Fin k, b i ^ ν i

@[simp]

theorem TauCeti.Huber.weightedEvalTerm_def {k : ℕ} {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (φ : A →+* B) (b : Fin k → B) (f : MvPowerSeries (Fin k) A) (ν : Fin k →₀ ℕ) : weightedEvalTerm φ b f ν = φ ((MvPowerSeries.coeff ν) f) * ∏ i : Fin k, b i ^ ν i

Unfolding lemma for TauCeti.Huber.weightedEvalTerm.

def TauCeti.Huber.IsWeightBounded {k : ℕ} {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [TopologicalSpace B] (φ : A →+* B) (T : Fin k → Set A) (b : Fin k → B) : Prop

The hypothesis on the tuple b: the weighted monomials φ(Tν) · bν, over all multi-indices at once, form a bounded subset of B.

This is Wedhorn's requirement that the variables be power-bounded relative to the weights, in the form the summability argument uses. It is a condition on the whole family rather than on each bᵢ separately, because the bound has to be uniform in ν. For the one-weight family T ≡ {1} it is equivalent to each bᵢ being power-bounded, which is Wedhorn's condition: every monomial bν lies in the pointwise product of the power-sets, and a finite pointwise product of bounded sets is bounded.

Equations

• TauCeti.Huber.IsWeightBounded φ T b = TauCeti.Huber.IsBounded (⋃ (ν : Fin k →₀ ℕ), (fun (t : A) => φ t * ∏ i : Fin k, b i ^ ν i) '' TauCeti.Huber.weightPow T ν)

theorem TauCeti.Huber.isWeightBounded_iff {k : ℕ} {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [TopologicalSpace B] (φ : A →+* B) (T : Fin k → Set A) (b : Fin k → B) : IsWeightBounded φ T b ↔ IsBounded (⋃ (ν : Fin k →₀ ℕ), (fun (t : A) => φ t * ∏ i : Fin k, b i ^ ν i) '' weightPow T ν)

Unfolding lemma for TauCeti.Huber.IsWeightBounded. The body is not exported, so this is how a consumer supplies one or takes one apart.

@[simp]

theorem TauCeti.Huber.isWeightBounded_one_weight_iff {k : ℕ} {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [TopologicalSpace B] (φ : A →+* B) (b : Fin k → B) : IsWeightBounded φ (fun (x : Fin k) => {1}) b ↔ IsBounded (Set.range fun (ν : Fin k →₀ ℕ) => ∏ i : Fin k, b i ^ ν i)

At the one-weight family the hypothesis is boundedness of the monomials. With every weight equal to {1} the weighted monomials are just the bν, so IsWeightBounded says exactly that they form a bounded set — the condition a reader expects to see, and the bridge from the roadmap's power-bounded-variable hypothesis.

theorem TauCeti.Huber.isWeightBounded_one_weight_iff_forall_isPowerBounded {k : ℕ} {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [TopologicalSpace B] (φ : A →+* B) (b : Fin k → B) : IsWeightBounded φ (fun (x : Fin k) => {1}) b ↔ ∀ (i : Fin k), IsPowerBounded (b i)

At the one-weight family the hypothesis is exactly Wedhorn's: the weighted monomials are bounded precisely when every variable is power-bounded.

This is the case in which the weights impose nothing, so the hypothesis on the tuple is the familiar one; for a general T it is TauCeti.Huber.IsWeightedVarPowerBounded that plays this role.

def TauCeti.Huber.weightedVar {k : ℕ} {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (φ : A →+* B) (T : Fin k → Set A) (b : Fin k → B) (i : Fin k) : Set B

The weighted variables of Proposition 5.50: the sets φ(Tᵢ) · bᵢ. The hypothesis 5.50 places on the tuple is about these, not about the bᵢ alone.

Equations

• TauCeti.Huber.weightedVar φ T b i = ⇑φ '' T i * {b i}

@[simp]

theorem TauCeti.Huber.weightedVar_def {k : ℕ} {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (φ : A →+* B) (T : Fin k → Set A) (b : Fin k → B) (i : Fin k) : weightedVar φ T b i = ⇑φ '' T i * {b i}

Unfolding lemma for TauCeti.Huber.weightedVar.

def TauCeti.Huber.IsWeightedVarPowerBounded {k : ℕ} {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [TopologicalSpace B] (φ : A →+* B) (T : Fin k → Set A) (b : Fin k → B) : Prop

Wedhorn's coordinatewise hypothesis: each weighted variable is power-bounded as a set, its powers all lying in one bounded subset of B.

This is the condition Proposition 5.50 actually states, one index at a time, and TauCeti.Huber.isWeightBounded_of_isWeightedVarPowerBounded derives the uniform bound TauCeti.Huber.IsWeightBounded from it. At the one-weight family weightedVar is {bᵢ}, so it reduces to each bᵢ being power-bounded.

Equations

• TauCeti.Huber.IsWeightedVarPowerBounded φ T b = ∀ (i : Fin k), TauCeti.Huber.IsBounded (⋃ (n : ℕ), TauCeti.Huber.weightedVar φ T b i ^ n)

theorem TauCeti.Huber.isWeightedVarPowerBounded_iff {k : ℕ} {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [TopologicalSpace B] (φ : A →+* B) (T : Fin k → Set A) (b : Fin k → B) : IsWeightedVarPowerBounded φ T b ↔ ∀ (i : Fin k), IsBounded (⋃ (n : ℕ), weightedVar φ T b i ^ n)

Unfolding lemma for TauCeti.Huber.IsWeightedVarPowerBounded. The body is not exported, so this is how a consumer supplies one or takes one apart.

theorem TauCeti.Huber.isWeightBounded_of_isWeightedVarPowerBounded {k : ℕ} {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [TopologicalSpace B] {φ : A →+* B} {T : Fin k → Set A} {b : Fin k → B} (h : IsWeightedVarPowerBounded φ T b) : IsWeightBounded φ T b

Wedhorn's coordinatewise hypothesis gives the uniform bound. Each weighted monomial set is a finite pointwise product of powers of the weighted variables, so it lies in the product of the bounded sets containing those powers — and a finite pointwise product of bounded sets is bounded.

This is what makes TauCeti.Huber.IsWeightBounded the right hypothesis for the summability theorem rather than a stronger one invented for it: the two are reached from the same place.

theorem TauCeti.Huber.weightedEvalTerm_mem_of_mem_weightMul {k : ℕ} {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] {φ : A →+* B} {T : Fin k → Set A} {b : Fin k → B} {U : AddSubgroup A} {V : Set B} {G : AddSubgroup B} {ν : Fin k →₀ ℕ} (hUV : ⇑φ '' ↑U ⊆ V) (hVG : V * (fun (t : A) => φ t * ∏ i : Fin k, b i ^ ν i) '' weightPow T ν ⊆ ↑G) {f : MvPowerSeries (Fin k) A} (hf : (MvPowerSeries.coeff ν) f ∈ weightMul T ν U) : weightedEvalTerm φ b f ν ∈ G

A coefficient bound gives a term bound, at a single multi-index: if the ν-th coefficient of f lies in Tν · U, and φ(U) times the weighted monomials at ν lands in the subgroup G, then the ν-th term of the evaluation lies in G. Both the hypothesis and the conclusion concern that one ν, and nothing topological is involved.

This is the estimate both convergence results run on. TauCeti.Huber.tendsto_weightedEvalTerm_cofinite_zero applies it to the cofinitely many coefficients that satisfy the bound; the continuity proof applies it to every coefficient at once.

theorem TauCeti.Huber.tendsto_weightedEvalTerm_cofinite_zero {k : ℕ} {A : Type u_1} {B : Type u_2} [CommRing A] [TopologicalSpace A] [CommRing B] [TopologicalSpace B] [NonarchimedeanAddGroup A] [NonarchimedeanAddGroup B] {φ : A →+* B} (hφ : ContinuousAt (⇑φ) 0) {T : Fin k → Set A} {b : Fin k → B} (hb : IsWeightBounded φ T b) {f : MvPowerSeries (Fin k) A} (hf : IsWeightedRestricted T f) : Filter.Tendsto (weightedEvalTerm φ b f) Filter.cofinite (nhds 0)

The terms of the evaluation tend to zero along the cofinite filter. This is the whole analytic input to summability — the convergence a summable family must have. It needs no completeness; completeness is what makes it sufficient, in TauCeti.Huber.summable_weightedEvalTerm.

The three hypotheses each do one thing: T-restrictedness puts all but finitely many coefficients into Tν · U, continuity of φ at zero makes U small enough that φ(U) shrinks the bounded family, and IsWeightBounded is what makes one U work for every ν at once.

theorem TauCeti.Huber.summable_weightedEvalTerm {k : ℕ} {A : Type u_1} {B : Type u_2} [CommRing A] [TopologicalSpace A] [NonarchimedeanAddGroup A] [CommRing B] [UniformSpace B] [IsUniformAddGroup B] [NonarchimedeanAddGroup B] [CompleteSpace B] {φ : A →+* B} (hφ : ContinuousAt (⇑φ) 0) {T : Fin k → Set A} {b : Fin k → B} (hb : IsWeightBounded φ T b) {f : MvPowerSeries (Fin k) A} (hf : IsWeightedRestricted T f) : Summable (weightedEvalTerm φ b f)

The evaluation of a T-restricted series is summable. Its terms tend to zero along the cofinite filter, which in a complete nonarchimedean group is summability.

theorem TauCeti.Huber.summable_weightedEvalTerm_of_isWeightedVarPowerBounded {k : ℕ} {A : Type u_1} {B : Type u_2} [CommRing A] [TopologicalSpace A] [NonarchimedeanAddGroup A] [CommRing B] [UniformSpace B] [IsUniformAddGroup B] [NonarchimedeanAddGroup B] [CompleteSpace B] {φ : A →+* B} (hφ : ContinuousAt (⇑φ) 0) {T : Fin k → Set A} {b : Fin k → B} (hb : IsWeightedVarPowerBounded φ T b) {f : MvPowerSeries (Fin k) A} (hf : IsWeightedRestricted T f) : Summable (weightedEvalTerm φ b f)

Summability under Wedhorn's coordinatewise hypothesis, for an arbitrary weight family: each weighted variable power-bounded as a set is enough. This is the theorem above read through TauCeti.Huber.isWeightBounded_of_isWeightedVarPowerBounded, and it is the form Proposition 5.50 states.

theorem TauCeti.Huber.summable_weightedEvalTerm_of_forall_isPowerBounded {k : ℕ} {A : Type u_1} {B : Type u_2} [CommRing A] [TopologicalSpace A] [NonarchimedeanAddGroup A] [CommRing B] [UniformSpace B] [IsUniformAddGroup B] [NonarchimedeanAddGroup B] [CompleteSpace B] {φ : A →+* B} (hφ : ContinuousAt (⇑φ) 0) {b : Fin k → B} (hb : ∀ (i : Fin k), IsPowerBounded (b i)) {f : MvPowerSeries (Fin k) A} (hf : IsWeightedRestricted (fun (x : Fin k) => {1}) f) : Summable (weightedEvalTerm φ b f)

Summability under Wedhorn's own hypothesis. At the one-weight family the condition on the tuple is that each variable be power-bounded, which is how Proposition 5.50 states it; this is the theorem above read through TauCeti.Huber.isWeightBounded_one_weight_iff_forall_isPowerBounded.