Coefficient-parametric transfinite character extension

This module contains the recursion shared by the integer and rational Wallace constructions. The coefficient-specific input is an additive character on one coordinate whose value at one is a prescribed circle element. The integer specialization uses scalar multiplication; the rational specialization obtains the character from Baer's extension theorem.

structure Wallace.CoefficientTransfiniteExtension.CoordinateExtension (R : Type w) [AddCommMonoid R] [One R] : Type w

A way to extend a prescribed circle value to a character on one coefficient coordinate.

• ofValue : UnitAddCircle → R →+ UnitAddCircle

  Build a coordinate character with the prescribed value at one.

• ofValue_one (t : UnitAddCircle) : (self.ofValue t) 1 = t

structure Wallace.CoefficientTransfiniteExtension.Data (R : Type w) (I : Type u) [Zero R] [LT I] : Type (max (max u (v + 1)) w)

The triangular data needed by the coefficient-parametric recursion.

• Code : Type v

  Codes for the prepared sequences.

• codeIndex : self.Code ↪ I

  The fresh coordinate assigned to a code.

• prepared : self.Code → ℕ → I →₀ R

  The sequence after finite block preprocessing.

• support_lt (c : self.Code) (n : ℕ) (i : I) : i ∈ (self.prepared c n).support → i < self.codeIndex c
• p : self.Code → Ultrafilter ℕ

  The ultrafilter along which the coded limit is imposed.

def Wallace.CoefficientTransfiniteExtension.ClosedUnderPreparedSupports {R : Type w} {I : Type u} [Zero R] [LT I] (E : Data R I) (D : Set I) : Prop

Closure under the prepared supports attached to code coordinates in D.

Equations

• Wallace.CoefficientTransfiniteExtension.ClosedUnderPreparedSupports E D = ∀ (c : E.Code), E.codeIndex c ∈ D → ∀ (n : ℕ), ∀ i ∈ (E.prepared c n).support, i ∈ D

def Wallace.CoefficientTransfiniteExtension.LocallyAdmissible {R : Type w} {I : Type u} [AddCommMonoid R] [One R] [LT I] (E : Data R I) (D : Set I) (character : (↑D →₀ R) →+ UnitAddCircle) : Prop

The local character already realizes each limit whose code coordinate lies in D.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Wallace.CoefficientTransfiniteExtension.finsuppAddHom {R : Type w} {I : Type u} [AddCommMonoid R] (coordinates : I → R →+ UnitAddCircle) : (I →₀ R) →+ UnitAddCircle

The character on a direct sum induced by its coordinate characters.

Equations

• Wallace.CoefficientTransfiniteExtension.finsuppAddHom coordinates = Finsupp.liftAddHom coordinates

def Wallace.CoefficientTransfiniteExtension.stageCoordinates {R : Type w} {I : Type u} [AddCommMonoid R] [LT I] [DecidableRel fun (x1 x2 : I) => x1 < x2] (i : I) (previous : (j : I) → j < i → R →+ UnitAddCircle) : I → R →+ UnitAddCircle

Totalize the coordinate characters available below a recursive stage.

Equations

• Wallace.CoefficientTransfiniteExtension.stageCoordinates i previous j = if h : j < i then previous j h else 0

noncomputable def Wallace.CoefficientTransfiniteExtension.stageEvaluation {R : Type w} {I : Type u} [AddCommMonoid R] [LT I] [DecidableRel fun (x1 x2 : I) => x1 < x2] (E : Data R I) (i : I) (previous : (j : I) → j < i → R →+ UnitAddCircle) (c : E.Code) (n : ℕ) : UnitAddCircle

Evaluate a prepared term using only coordinates below the current stage.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Wallace.CoefficientTransfiniteExtension.compactStageLimit {R : Type w} {I : Type u} [AddCommMonoid R] [LT I] [DecidableRel fun (x1 x2 : I) => x1 < x2] (E : Data R I) (i : I) (previous : (j : I) → j < i → R →+ UnitAddCircle) (c : E.Code) : UnitAddCircle

The compact ultrafilter limit selected at a code coordinate.

Equations

• Wallace.CoefficientTransfiniteExtension.compactStageLimit E i previous c = (Ultrafilter.map (Wallace.CoefficientTransfiniteExtension.stageEvaluation E i previous c) (E.p c)).lim

noncomputable def Wallace.CoefficientTransfiniteExtension.coordinateStep {R : Type w} {I : Type u} [AddCommMonoid R] [One R] [LinearOrder I] (extension : CoordinateExtension R) (E : Data R I) (D : Set I) (character : (↑D →₀ R) →+ UnitAddCircle) (i : I) (previous : (j : I) → j < i → R →+ UnitAddCircle) : R →+ UnitAddCircle

One step of the well-founded coordinate recursion.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Wallace.CoefficientTransfiniteExtension.globalCoordinate {R : Type w} {I : Type u} [AddCommMonoid R] [One R] [LinearOrder I] [WellFoundedLT I] (extension : CoordinateExtension R) (E : Data R I) (D : Set I) (character : (↑D →₀ R) →+ UnitAddCircle) : I → R →+ UnitAddCircle

The coordinate characters constructed by well-founded recursion.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Wallace.CoefficientTransfiniteExtension.globalCharacter {R : Type w} {I : Type u} [AddCommMonoid R] [One R] [LinearOrder I] [WellFoundedLT I] (extension : CoordinateExtension R) (E : Data R I) (D : Set I) (character : (↑D →₀ R) →+ UnitAddCircle) : (I →₀ R) →+ UnitAddCircle

The global character assembled from the recursively constructed coordinates.

Equations

• One or more equations did not get rendered due to their size.

theorem Wallace.CoefficientTransfiniteExtension.globalCharacter_eq_local_restriction {R : Type w} {I : Type u} [AddCommMonoid R] [One R] [LinearOrder I] [WellFoundedLT I] (extension : CoordinateExtension R) (E : Data R I) (D : Set I) (character : (↑D →₀ R) →+ UnitAddCircle) (x : I →₀ R) (hx : ∀ i ∈ x.support, i ∈ D) : (globalCharacter extension E D character) x = character (Finsupp.subtypeDomain D x)

theorem Wallace.CoefficientTransfiniteExtension.globalCharacter_admissible {R : Type w} {I : Type u} [AddCommMonoid R] [One R] [LinearOrder I] [WellFoundedLT I] (extension : CoordinateExtension R) (E : Data R I) (D : Set I) (character : (↑D →₀ R) →+ UnitAddCircle) (hclosed : ClosedUnderPreparedSupports E D) (hlocal : LocallyAdmissible E D character) (c : E.Code) : Filter.Tendsto (fun (n : ℕ) => (globalCharacter extension E D character) (E.prepared c n)) (↑(E.p c)) (nhds ((globalCharacter extension E D character) (Finsupp.single (E.codeIndex c) 1)))

The transfinite extension realizes every prescribed ultrafilter limit.