OAI/Analysis/NuclearUltrapower/CuntzWords.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.NuclearUltrapower.CuntzWords.Word line 13

   Source documentation

   Fixed-length binary words, with a product decomposition at every successor.

   @[reducible] def Word : ℕ → Type
     | 0 => PUnit
     | n+1 => Fin 2 × Word n

2. instance OAI.NuclearUltrapower.CuntzWords.(instance at line 17) line 17
3. instance OAI.NuclearUltrapower.CuntzWords.(instance at line 24) line 24
4. def OAI.NuclearUltrapower.CuntzWords.value line 26
5. theorem OAI.NuclearUltrapower.CuntzWords.value_zero line 30
6. theorem OAI.NuclearUltrapower.CuntzWords.value_succ line 32
7. def OAI.NuclearUltrapower.CuntzWords.index line 35
8. theorem OAI.NuclearUltrapower.CuntzWords.index_succ line 39
9. theorem OAI.NuclearUltrapower.CuntzWords.index_height line 42
10. theorem OAI.NuclearUltrapower.CuntzWords.index_injective line 49
11. theorem OAI.NuclearUltrapower.CuntzWords.index_ne_of_length_ne line 62
12. theorem OAI.NuclearUltrapower.CuntzWords.cross line 70

    Source documentation

    Orthogonality is a consequence of the two defining Cuntz relations.

    theorem cross {D : Type*} [CStarAlgebra D] (r : Fin 2 → D) (hr : CuntzTwoRelations r)
        (i j : Fin 2) (hij : i ≠ j) : star (r i) * r j = 0 := by
    …

    Mentions: OAI.NuclearUltrapower.CuntzTwoRelations

13. theorem OAI.NuclearUltrapower.CuntzWords.sum_range line 88

    Source documentation

    Completeness of the finite-length row is proved, not assumed.

    theorem sum_range {D : Type*} [CStarAlgebra D] (r : Fin 2 → D) (hr : CuntzTwoRelations r)
        (n : ℕ) : ∑ w : Word n, value r w * star (value r w) = 1 := by
    …

    Mentions: OAI.NuclearUltrapower.CuntzTwoRelations, OAI.NuclearUltrapower.CuntzWords.Word, OAI.NuclearUltrapower.CuntzWords.value

14. abbrev OAI.NuclearUltrapower.CuntzAveraging.Target line 120
15. def OAI.NuclearUltrapower.CuntzAveraging.coordinate line 123
16. theorem OAI.NuclearUltrapower.CuntzAveraging.coordinate_apply line 126
17. theorem OAI.NuclearUltrapower.CuntzAveraging.inner_coordinate line 129
18. theorem OAI.NuclearUltrapower.CuntzAveraging.coordinate_norm line 135
19. def OAI.NuclearUltrapower.CuntzAveraging.left line 141
20. def OAI.NuclearUltrapower.CuntzAveraging.right line 142
21. theorem OAI.NuclearUltrapower.CuntzAveraging.left_coordinate line 144
22. theorem OAI.NuclearUltrapower.CuntzAveraging.right_coordinate line 150
23. theorem OAI.NuclearUltrapower.CuntzAveraging.left_star_mul line 156
24. theorem OAI.NuclearUltrapower.CuntzAveraging.left_norm_le line 165
25. theorem OAI.NuclearUltrapower.CuntzAveraging.right_norm_le line 172
26. def OAI.NuclearUltrapower.CuntzAveraging.row line 189
27. theorem OAI.NuclearUltrapower.CuntzAveraging.row_apply line 192
28. theorem OAI.NuclearUltrapower.CuntzAveraging.row_support line 196
29. theorem OAI.NuclearUltrapower.CuntzAveraging.inner_row line 205
30. theorem OAI.NuclearUltrapower.CuntzAveraging.inner_row_ne line 218
31. theorem OAI.NuclearUltrapower.CuntzAveraging.support_inner line 223
32. theorem OAI.NuclearUltrapower.CuntzAveraging.row_norm line 231
33. theorem OAI.NuclearUltrapower.CuntzAveraging.support_norm_le line 235
34. theorem OAI.NuclearUltrapower.CuntzAveraging.row_norm_le line 239
35. theorem OAI.NuclearUltrapower.CuntzAveraging.row_step line 246

    Source documentation

    The row recursion comes from word concatenation and the genuine model shifts.

    theorem row_step (n : ℕ) : row R (n+1) =
        ∑ i : Fin 2, ((left i).comp (row R n)).comp (star (R (generator i))) := by
    …

    Mentions: OAI.NuclearUltrapower.CuntzAveraging.row, OAI.NuclearUltrapower.CuntzAveraging.left

36. theorem OAI.NuclearUltrapower.CuntzAveraging.rep_cross line 256
37. theorem OAI.NuclearUltrapower.CuntzAveraging.row_next_generator line 265

    Source documentation

    Exact finite-level intertwining of each Cuntz generator.

    theorem row_next_generator (n : ℕ) (i : Fin 2) :
        (row R (n+1)).comp (R (generator i)) = (left i).comp (row R n) := by
    …

    Mentions: OAI.NuclearUltrapower.CuntzAveraging.row, OAI.NuclearUltrapower.CuntzAveraging.left

38. theorem OAI.NuclearUltrapower.CuntzAveraging.left_star_row_next line 280

    Source documentation

    Exact finite-level intertwining of the adjoint generator in reverse.

    theorem left_star_row_next (n : ℕ) (i : Fin 2) :
        (star (left i)).comp (row R (n+1)) = (row R n).comp (star (R (generator i))) := by
    …

    Mentions: OAI.NuclearUltrapower.CuntzAveraging.left, OAI.NuclearUltrapower.CuntzAveraging.row

39. theorem OAI.NuclearUltrapower.CuntzAveraging.row_commuting line 294

    Source documentation

    Arbitrary commuting operators intertwine with the second tensor coordinate.

    theorem row_commuting (n : ℕ) (T : H →L[ℂ] H)
        (hT : ∀ a, Commute (R a) T) : (row R n).comp T = (right T).comp (row R n) := by
    …

    Mentions: OAI.NuclearUltrapower.CuntzAveraging.row, OAI.NuclearUltrapower.CuntzAveraging.right