Assembly.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Fresh bundle maps and assembly of the test-bundle step.

theorem OAI.Kaplansky.testBundleSlot_card line 16
abbrev OAI.Kaplansky.TestSourceCoordinates line 20
abbrev OAI.Kaplansky.TestFreshRank line 25
abbrev OAI.Kaplansky.TestFreshCoordinates line 27
theorem OAI.Kaplansky.exists_test_eight_fresh_bundle_maps line 32

theorem OAI.Kaplansky.exists_smoothTest_freshMaps line 59

Source documentation

The finite-coordinate incidence maps give genuine continuous maps on the original Hilbert-sum presentation of E_j and its fresh block.

theorem exists_smoothTest_freshMaps {m R j : ℕ} (hm : 0<m) (hj : j<R) :
    ∃ A : ∀ y, Fin 8 → SmoothTestBundle m R (j+1) j hj (Nat.le_succ j) y →ₗ[ℂ]
      (smoothFreshCore m R j hj).Fiber y,
      (∀ i, Continuous (fun z : TotalSpace (EuclideanSpace ℂ (TestBundleSlot m R j))
        (SmoothTestBundle m R (j+1) j hj (Nat.le_succ j)) =>
        TotalSpace.mk' (EuclideanSpace ℂ (Fin (TestFreshRank m R j))) z.proj (A z.proj i z.2))) ∧
      ∀ y (S : Submodule ℂ (SmoothTestBundle m R (j+1) j hj (Nat.le_succ j) y)),
        m<finrank ℂ S → 2*finrank ℂ S≤finrank ℂ
          (⨆ i, S.map (A y i) : Submodule ℂ ((smoothFreshCore m R j hj).Fiber y)) := by
…

Mentions: OAI.Kaplansky.SmoothTestBundle, OAI.Kaplansky.smoothFreshCore, OAI.Kaplansky.TestBundleSlot, OAI.Kaplansky.TestFreshRank

abbrev OAI.Kaplansky.TestNextSlot line 108
def OAI.Kaplansky.testNextLabel line 111
def OAI.Kaplansky.smoothNextCore line 115
Source documentation
E_{j+1} presented as the direct sum of its replacement and fresh blocks.
```
def smoothNextCore (m R j : ℕ) (hj : j<R) :=
…
```
theorem OAI.Kaplansky.testNextSlot_card line 118
theorem OAI.Kaplansky.exists_test_twentyFour_expanding_maps line 132