The evaluation of a weighted restricted power series

TauCeti/RingTheory/Huber/WeightedEval/Basic.lean proves that the terms φ(coeff ν f) · bν of Wedhorn's evaluation (Proposition 5.50) are summable. This file takes their sum and gives it the API a universal property needs: the value on a constant series, the value on a variable, and additivity in the series.

Multiplicativity is not proved here. weightedEval (f * g) = weightedEval f * weightedEval g is a Cauchy-product argument — the coefficients of f * g are sums over the antidiagonal, so the statement is a reindexing of a double sum rather than a consequence of anything below — and it is the remaining step before 5.50 can be stated as a universal property.

Main definitions

• TauCeti.Huber.weightedEval: the sum ∑' ν, φ(coeff ν f) · bν.

Main results

• TauCeti.Huber.weightedEval_monomial, with TauCeti.Huber.weightedEval_C and TauCeti.Huber.weightedEval_X as its cases at ν = 0 and ν = single i 1: the value on a monomial is its own term, which is what makes this the evaluation at b. These, and the value on 0, are unconditional: each of the three term families is supported on at most one index — the zero series gives the family that vanishes identically — so the sum is a single term and no summability hypothesis is involved.
• TauCeti.Huber.hasSum_weightedEval: under the hypotheses of the summability theorem, the terms have weightedEval as their sum. This is the consumer-facing statement — it names the sum instead of leaving a tsum to be manipulated — and is not itself used below.
• TauCeti.Huber.weightedEval_zero and TauCeti.Huber.weightedEval_add_of_summable: the evaluation is additive in the series, the latter stated where additivity is actually true — two summable term families, with no weights, completeness or restrictedness in sight. TauCeti.Huber.weightedEval_add and its corollaries are that composed with a way of producing summability.

References

• Wedhorn, Adic Spaces, Proposition 5.50.

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

Wedhorn's evaluation of a series at a tuple b along φ: the sum of the terms φ(coeff ν f) · bν.

Unconditionally a tsum, so it is junk when the family is not summable. The results that take a genuine infinite sum — TauCeti.Huber.weightedEval_add and its corollaries — therefore obtain summability from TauCeti.Huber.summable_weightedEvalTerm and pass it to TauCeti.Huber.weightedEval_add_of_summable. The values on 0, on a constant and on a variable need none of that: their term families are supported on at most one index, so the sum is read off that index directly.

Equations

• TauCeti.Huber.weightedEval φ b f = ∑' (ν : Fin k →₀ ℕ), TauCeti.Huber.weightedEvalTerm φ b f ν

theorem TauCeti.Huber.weightedEval_def {k : ℕ} {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [TopologicalSpace B] (φ : A →+* B) (b : Fin k → B) (f : MvPowerSeries (Fin k) A) : weightedEval φ b f = ∑' (ν : Fin k →₀ ℕ), weightedEvalTerm φ b f ν

Unfolding lemma for TauCeti.Huber.weightedEval.

@[simp]

theorem TauCeti.Huber.weightedEval_zero {k : ℕ} {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [TopologicalSpace B] (φ : A →+* B) (b : Fin k → B) : weightedEval φ b 0 = 0

The evaluation of the zero series is zero.

@[simp]

theorem TauCeti.Huber.weightedEval_monomial {k : ℕ} {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [TopologicalSpace B] (φ : A →+* B) (b : Fin k → B) (ν : Fin k →₀ ℕ) (a : A) : weightedEval φ b ((MvPowerSeries.monomial ν) a) = φ a * ∏ i : Fin k, b i ^ ν i

The evaluation of a monomial is its term. Every other coefficient of monomial ν a vanishes, so the sum collapses to the index ν. The values on a constant and on a variable are the two special cases below.

@[simp]

theorem TauCeti.Huber.weightedEval_C {k : ℕ} {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [TopologicalSpace B] (φ : A →+* B) (b : Fin k → B) (a : A) : weightedEval φ b (MvPowerSeries.C a) = φ a

The evaluation sends a constant series to its image, the monomial at ν = 0.

@[simp]

theorem TauCeti.Huber.weightedEval_X {k : ℕ} {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [TopologicalSpace B] (φ : A →+* B) (b : Fin k → B) (i : Fin k) : weightedEval φ b (MvPowerSeries.X i) = b i

The evaluation sends a variable to its value, the monomial at ν = single i 1.

theorem TauCeti.Huber.weightedEval_add_of_summable {k : ℕ} {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [TopologicalSpace B] [ContinuousAdd B] [T2Space B] {φ : A →+* B} {b : Fin k → B} {f g : MvPowerSeries (Fin k) A} (hf : Summable (weightedEvalTerm φ b f)) (hg : Summable (weightedEvalTerm φ b g)) : weightedEval φ b (f + g) = weightedEval φ b f + weightedEval φ b g

The evaluation is additive in the series, at the level where that is actually true: two summable term families. Nothing topological about A, no completeness, no weights and no restrictedness enter — those hypotheses exist only to produce summability, and every additivity result below is this one composed with a way of producing it.

Both summability hypotheses are needed: a sum of two families is the sum of their sums only when each converges.

theorem TauCeti.Huber.hasSum_weightedEval {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} {T : Fin k → Set A} {b : Fin k → B} (hφ : ContinuousAt (⇑φ) 0) (hb : IsWeightBounded φ T b) {f : MvPowerSeries (Fin k) A} (hf : IsWeightedRestricted T f) : HasSum (weightedEvalTerm φ b f) (weightedEval φ b f)

The terms sum to the evaluation. This is for consumers: it names the sum, so that a caller holding the summability hypotheses does not have to manipulate a tsum. Nothing in this file uses it — additivity goes through TauCeti.Huber.weightedEval_add_of_summable, which asks only for Summable.

theorem TauCeti.Huber.hasSum_weightedEval_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} {T : Fin k → Set A} {b : Fin k → B} (hφ : ContinuousAt (⇑φ) 0) (hb : IsWeightedVarPowerBounded φ T b) {f : MvPowerSeries (Fin k) A} (hf : IsWeightedRestricted T f) : HasSum (weightedEvalTerm φ b f) (weightedEval φ b f)

TauCeti.Huber.hasSum_weightedEval under Wedhorn's coordinatewise hypothesis.

theorem TauCeti.Huber.hasSum_weightedEval_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} {b : Fin k → B} (hφ : ContinuousAt (⇑φ) 0) (hb : ∀ (i : Fin k), IsPowerBounded (b i)) {f : MvPowerSeries (Fin k) A} (hf : IsWeightedRestricted (fun (x : Fin k) => {1}) f) : HasSum (weightedEvalTerm φ b f) (weightedEval φ b f)

TauCeti.Huber.hasSum_weightedEval at the one-weight family, where the hypothesis is that each variable is power-bounded.

theorem TauCeti.Huber.weightedEval_add {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} {T : Fin k → Set A} {b : Fin k → B} [T2Space B] (hφ : ContinuousAt (⇑φ) 0) (hb : IsWeightBounded φ T b) {f g : MvPowerSeries (Fin k) A} (hf : IsWeightedRestricted T f) (hg : IsWeightedRestricted T g) : weightedEval φ b (f + g) = weightedEval φ b f + weightedEval φ b g

The evaluation is additive on T-restricted series. This is TauCeti.Huber.weightedEval_add_of_summable with summability supplied by TauCeti.Huber.summable_weightedEvalTerm.

theorem TauCeti.Huber.weightedEval_add_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} {T : Fin k → Set A} {b : Fin k → B} [T2Space B] (hφ : ContinuousAt (⇑φ) 0) (hb : IsWeightedVarPowerBounded φ T b) {f g : MvPowerSeries (Fin k) A} (hf : IsWeightedRestricted T f) (hg : IsWeightedRestricted T g) : weightedEval φ b (f + g) = weightedEval φ b f + weightedEval φ b g

TauCeti.Huber.weightedEval_add under Wedhorn's coordinatewise hypothesis.

theorem TauCeti.Huber.weightedEval_add_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} {b : Fin k → B} [T2Space B] (hφ : ContinuousAt (⇑φ) 0) (hb : ∀ (i : Fin k), IsPowerBounded (b i)) {f g : MvPowerSeries (Fin k) A} (hf : IsWeightedRestricted (fun (x : Fin k) => {1}) f) (hg : IsWeightedRestricted (fun (x : Fin k) => {1}) g) : weightedEval φ b (f + g) = weightedEval φ b f + weightedEval φ b g

TauCeti.Huber.weightedEval_add at the one-weight family.