Sequence.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Prefix and full test steps, pullbacks, and the infinite test sequence.

def OAI.Kaplansky.lineSumPullbackStep line 19

Source documentation

Pull continuous normalized maps from a projective subproduct to the full product. Continuity uses the actual line-sum pullback topology.

def lineSumPullbackStep {ι κ S T : Type*} [Fintype ι] [Fintype κ] [Fintype S] [Fintype T]
    (K : κ → ℕ) (f : ι → κ) (a : S → Option ι) (b : T → Option ι)
    (X : ContinuousNormalizedStep (EuclideanSpace ℂ S) (EuclideanSpace ℂ T)
      (SmoothLineSumBundle (fun i => K (f i)) a) (SmoothLineSumBundle (fun i => K (f i)) b)) :
    ContinuousNormalizedStep (EuclideanSpace ℂ S) (EuclideanSpace ℂ T)
      (SmoothLineSumBundle K (fun s => (a s).map f))
      (SmoothLineSumBundle K (fun t => (b t).map f)) where
…

Mentions: OAI.Kaplansky.ContinuousNormalizedStep

theorem OAI.Kaplansky.testCoordinateStep_nonempty line 48
Source documentation
The previously constructed normalized tuple, including both directions of continuity and the actual adjoint identity.
```
theorem testCoordinateStep_nonempty {m R j : ℕ} (hm : 0<m) (hj : j<R) :
    Nonempty (TestCoordinateStepType m R j hj) := by
…
```
Mentions: OAI.Kaplansky.TestCoordinateStepType
def OAI.Kaplansky.testCoordinateStep line 61
def OAI.Kaplansky.testPrefixStep line 64
theorem OAI.Kaplansky.testSummandLineIndex_map line 77
abbrev OAI.Kaplansky.FullTestBundle line 83
Source documentation
A single coherent presentation of the finite stages on full Y.
```
abbrev FullTestBundle (m R j : ℕ) (hj : j≤R) :=
…
```
def OAI.Kaplansky.testFullStep line 86
def OAI.Kaplansky.testLineStage line 105
def OAI.Kaplansky.testSequenceStage line 108
theorem OAI.Kaplansky.testSequenceStage_prefix line 112
theorem OAI.Kaplansky.testSequenceStage_tail line 115
def OAI.Kaplansky.testSequenceStep line 126
Source documentation
All 24 normalized bundle maps for all levels, constructed solely from m>0. Both forward maps and their genuine adjoints are continuous over the single full projective product Y.
```
def testSequenceStep {m R : ℕ} (hm : 0<m) (j : ℕ) :
    (testSequenceStage m R j).Step (testSequenceStage m R (j+1)) := by
…
```
Mentions: OAI.Kaplansky.testSequenceStage
theorem OAI.Kaplansky.testSequenceStage_rank line 137
theorem OAI.Kaplansky.testSequenceStage_tail_rank line 143
theorem OAI.Kaplansky.smoothTestBundle_zero_baseSet line 159
def OAI.Kaplansky.smoothTestBundleZeroTotalHomeomorph line 176
Source documentation
A global linear chart for the actual full-product E₀, identifying it with Y times its Hilbert fiber, with exactly d₀ coordinates.
```
def smoothTestBundleZeroTotalHomeomorph (m R : ℕ) :
    TotalSpace (EuclideanSpace ℂ (TestBundleSlot m R 0)) (FullTestBundle m R 0 (Nat.zero_le R)) ≃ₜ
      SmoothTestBase m R × EuclideanSpace ℂ (TestBundleSlot m R 0) := by
…
```
Mentions: OAI.Kaplansky.TestBundleSlot, OAI.Kaplansky.FullTestBundle, OAI.Kaplansky.SmoothTestBase
theorem OAI.Kaplansky.smoothTestBundleZeroTotalHomeomorph_apply line 186