Transfinite extension of an integer-valued local character

This file specializes the coefficient-parametric Wallace recursion to the free Abelian group. An integer coordinate character is uniquely determined by its value at one.

def Wallace.TransfiniteExtension.integerCoordinateExtension : CoefficientTransfiniteExtension.CoordinateExtension ℤ

Extend a prescribed circle value to the corresponding integer character.

Equations

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

@[reducible, inline]

abbrev Wallace.TransfiniteExtension.Data (I : Type u) [LT I] : Type (max (max u (u_1 + 1)) 0)

Triangular data for integer-valued prepared sequences.

Equations

• Wallace.TransfiniteExtension.Data I = Wallace.CoefficientTransfiniteExtension.Data ℤ I

@[reducible, inline]

abbrev Wallace.TransfiniteExtension.ClosedUnderPreparedSupports {I : Type u} [LT I] (E : Data I) (D : Set I) : Prop

Closure under the integer prepared supports associated to local code coordinates.

Equations

• Wallace.TransfiniteExtension.ClosedUnderPreparedSupports E D = Wallace.CoefficientTransfiniteExtension.ClosedUnderPreparedSupports E D

@[reducible, inline]

abbrev Wallace.TransfiniteExtension.LocallyAdmissible {I : Type u} [LT I] (E : Data I) (D : Set I) (character : (↑D →₀ ℤ) →+ UnitAddCircle) : Prop

The local integer character realizes every limit whose code coordinate is local.

Equations

• Wallace.TransfiniteExtension.LocallyAdmissible E D character = Wallace.CoefficientTransfiniteExtension.LocallyAdmissible E D character

@[reducible, inline]

noncomputable abbrev Wallace.TransfiniteExtension.globalCharacter {I : Type u} [LinearOrder I] [WellFoundedLT I] (E : Data I) (D : Set I) (character : (↑D →₀ ℤ) →+ UnitAddCircle) : (I →₀ ℤ) →+ UnitAddCircle

The global integer character produced by the shared transfinite recursion.

Equations

• Wallace.TransfiniteExtension.globalCharacter E D character = Wallace.CoefficientTransfiniteExtension.globalCharacter Wallace.TransfiniteExtension.integerCoordinateExtension E D character

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

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

@[reducible, inline]

abbrev Wallace.TransfiniteExtension.ContinuumData : Type (u_1 + 1)

Integer transfinite-extension data over the canonical continuum index.

Equations

• Wallace.TransfiniteExtension.ContinuumData = Wallace.TransfiniteExtension.Data Wallace.TriangularPreprocess.ContinuumIndex