OAI/Analysis/Kaplansky/TestAlgebra.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Kaplansky.ActualTestIndex line 18
2. instance OAI.Kaplansky.(instance at line 20) line 20
3. abbrev OAI.Kaplansky.ActualTestFiber line 23
4. instance OAI.Kaplansky.actualTestFiber_zero_nontrivial line 26
5. def OAI.Kaplansky.actualTestOperator line 35

   Source documentation

   Actual bounded blocks of the normalized bundle test, at all levels.

   def actualTestOperator (i : Fin 24) (z : ActualTestIndex) (j : ℕ) :
       ActualTestFiber z j →L[ℂ] ActualTestFiber z (j+1) := by
   …

   Mentions: OAI.Kaplansky.ActualTestIndex, OAI.Kaplansky.ActualTestFiber

6. theorem OAI.Kaplansky.actualTestOperator_column line 41
7. theorem OAI.Kaplansky.actualTestOperator_row line 50
8. theorem OAI.Kaplansky.actualTestOperator_norm line 59
9. def OAI.Kaplansky.actualTestWord line 69
10. theorem OAI.Kaplansky.actualTestWord_level_le line 72
11. theorem OAI.Kaplansky.actualTestWord_continuous line 75
12. theorem OAI.Kaplansky.actualTestWord_shift_eval line 83

    Source documentation

    Exact agreement with the actual operators used in the constructed bounded-product algebra; this includes constants and every adjoint case.

    theorem actualTestWord_shift_eval (z : ActualTestIndex) (w : List (Bool × Fin 24))
        (v : ActualTestFiber z 0) :
        applyWord (shiftLetter (fun i j => actualTestOperator i z j)
          (fun i j => actualTestOperator_norm i z j)) w (lp.single 2 0 v) =
          lp.single 2 (actualTestWord (R := z.2.1.val) z.1.property w).level
    …

    Mentions: OAI.Kaplansky.ActualTestIndex, OAI.Kaplansky.ActualTestFiber, OAI.Kaplansky.applyWord, OAI.Kaplansky.shiftLetter, OAI.Kaplansky.actualTestOperator, OAI.Kaplansky.actualTestOperator_norm, OAI.Kaplansky.actualTestWord

13. theorem OAI.Kaplansky.actualTestPolynomial_from_bottom line 92

    Source documentation

    The finite degree restriction for all actual test coordinates.

    theorem actualTestPolynomial_from_bottom (z : ActualTestIndex) {J : Type*}
        (s : Finset J) (w : J → List (Bool × Fin 24)) (c : J → ℂ)
        (hdeg : ∀ j ∈ s, (w j).length ≤ z.2.1.val) (v : ActualTestFiber z 0) :
        (∑ j ∈ s, c j • applyWord (shiftLetter (fun i k => actualTestOperator i z k)
          (fun i k => actualTestOperator_norm i z k)) (w j) (lp.single 2 0 v)) ∈
          hilbertLevels z.2.1.val :=
    …

    Mentions: OAI.Kaplansky.ActualTestIndex, OAI.Kaplansky.ActualTestFiber, OAI.Kaplansky.applyWord, OAI.Kaplansky.shiftLetter, OAI.Kaplansky.actualTestOperator, OAI.Kaplansky.actualTestOperator_norm, OAI.Kaplansky.hilbertLevels

14. instance OAI.Kaplansky.actualHilbert_nontrivial line 104
15. abbrev OAI.Kaplansky.ActualHilbert line 107
16. def OAI.Kaplansky.actualBoundedGenerator line 109
17. abbrev OAI.Kaplansky.ActualAlgebra line 113
18. theorem OAI.Kaplansky.actual_test_shift_algebra line 115
19. def OAI.Kaplansky.actualRepresentation line 131
20. theorem OAI.Kaplansky.actualRepresentation_generator line 140
21. theorem OAI.Kaplansky.actualRepresentation_norm line 144
22. abbrev OAI.Kaplansky.actualAlgebra_cstar line 148
23. theorem OAI.Kaplansky.actualAlgebra_nontrivial_separable line 150