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
def Wallace.RationalTransfiniteExtension.integerCircleHom (t : UnitAddCircle) :
ℤ →+ UnitAddCircle

The integer character with prescribed value at one.

Equations
Instances For
    source
    noncomputable def Wallace.RationalTransfiniteExtension.extendRationalCoordinate (t : UnitAddCircle) :
    ℚ →+ UnitAddCircle

    An additive homomorphism on ℚ extending the integer character with value t at one.

    Equations
    Instances For
      source
      noncomputable def Wallace.RationalTransfiniteExtension.rationalCoordinateExtension :
      CoefficientTransfiniteExtension.CoordinateExtension ℚ

      Baer's extension supplies the coordinate extension used by the generic recursion.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        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