OAI/Analysis/Kaplansky/MatrixImage.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kaplansky.stageModelBasis line 18
2. def OAI.Kaplansky.trivialMapFrame line 25

   Source documentation

   Columns of a continuous injective map from a genuinely trivial stage are a continuous independent frame of its image.

   def trivialMapFrame (L : ContinuousStageMap a b) (ha : ∀ s, a.label s=none)
       (y₀ : ProjectiveProduct K) (hinj : ∀ y, Function.Injective (L.map y)) :
       ContinuousIndependentStageFrame b (Fintype.card a.Slot) where
   …

   Mentions: OAI.Kaplansky.ContinuousStageMap, OAI.Kaplansky.ContinuousIndependentStageFrame

3. theorem OAI.Kaplansky.span_basis_image line 34
4. theorem OAI.Kaplansky.trivialMapFrame_span line 40
5. def OAI.Kaplansky.trivialMapImageHomeomorph line 49
6. theorem OAI.Kaplansky.norm_lower_bound_injective line 60
7. theorem OAI.Kaplansky.actualInput_label_none line 71

   Source documentation

   All matrix input coordinates are actual copies of E₀.

   theorem actualInput_label_none (m n R : ℕ)
       (s : (towerInputStage (testSequenceStage m R) n).Slot) :
       (towerInputStage (testSequenceStage m R) n).label s=none := by
   …

   Mentions: OAI.Kaplansky.towerInputStage, OAI.Kaplansky.testSequenceStage

8. def OAI.Kaplansky.actualInputTrivialization line 83
9. theorem OAI.Kaplansky.actualInput_finrank line 90
10. def OAI.Kaplansky.actualRetainedUnitary line 104
11. def OAI.Kaplansky.actualMatrixRestriction line 124

    Source documentation

    The actual finite rectangular matrix map into G, constructed from all its polynomial terms. This definition assumes no obstruction or lower bound.

    def actualMatrixRestriction {m n R : ℕ} (hm : 0<m) {T : Type*}
        (s : Finset T) (t : T → BoundedMatrixTerm m n R) (y : SmoothTestBase m R) :
        (towerInputStage (testSequenceStage m R) n).Fiber y →ₗ[ℂ] RetainedBundle m R y :=
    …

    Mentions: OAI.Kaplansky.BoundedMatrixTerm, OAI.Kaplansky.SmoothTestBase, OAI.Kaplansky.towerInputStage, OAI.Kaplansky.testSequenceStage, OAI.Kaplansky.RetainedBundle

12. theorem OAI.Kaplansky.actualMatrixRestriction_continuous line 130
13. def OAI.Kaplansky.retainedLineStage line 139
14. def OAI.Kaplansky.actualMatrixStageMap line 142
15. theorem OAI.Kaplansky.actualMatrixRestriction_lower_bound line 147
16. def OAI.Kaplansky.actualMatrixImageHomeomorph line 158
17. theorem OAI.Kaplansky.actualMatrixImage_finrank line 170