Documentation

LeanPool.Wallace.RationalTransfiniteExtension

Transfinite extension for the rational direct sum #

This file supplies the coefficient-specific input to the shared transfinite recursion. Baer's extension theorem extends the integer character with prescribed value at one to a character on each rational coordinate.

source
@[reducible, inline]
abbrev Wallace.RationalTransfiniteExtension.Data (I : Type u) [LT I] :
Type (max (max u (u_1 + 1)) 0)

Triangular data for rational-valued prepared sequences.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev Wallace.RationalTransfiniteExtension.ClosedUnderPreparedSupports {I : Type u} [LT I] (E : Data I) (D : Set I) :
    Prop

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

    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev Wallace.RationalTransfiniteExtension.LocallyAdmissible {I : Type u} [LT I] (E : Data I) (D : Set I) (character : (↑D →₀ ℚ) →+ UnitAddCircle) :
      Prop

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

      Equations
      Instances For
        source
        @[reducible, inline]
        noncomputable abbrev Wallace.RationalTransfiniteExtension.globalCharacter {I : Type u} [LinearOrder I] [WellFoundedLT I] (E : Data I) (D : Set I) (character : (↑D →₀ ℚ) →+ UnitAddCircle) :
        (I →₀ ℚ) →+ UnitAddCircle

        The global rational character produced by the shared transfinite recursion.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem Wallace.RationalTransfiniteExtension.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)
          source
          theorem Wallace.RationalTransfiniteExtension.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)))
          source
          @[reducible, inline]
          abbrev Wallace.RationalTransfiniteExtension.ContinuumData :
          Type (u_1 + 1)

          Rational transfinite-extension data over the canonical continuum index.

          Equations
          Instances For