OAI/Analysis/NuclearUltrapower/CuntzAlgebra.lean

GitHub source file

69 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.NuclearUltrapower.CuntzModel.Index line 14
2. abbrev OAI.NuclearUltrapower.CuntzModel.Space line 15
3. def OAI.NuclearUltrapower.CuntzModel.shiftIndex line 20

   Source documentation

   Integer height separates words of different lengths; the binary coordinate partitions every level into the two isometric ranges.

   def shiftIndex (i : Fin 2) : Index ↪ Index where
   …

   Mentions: OAI.NuclearUltrapower.CuntzModel.Index

4. theorem OAI.NuclearUltrapower.CuntzModel.shiftIndex_apply line 29
5. theorem OAI.NuclearUltrapower.CuntzModel.shiftIndex_disjoint line 32
6. theorem OAI.NuclearUltrapower.CuntzModel.shiftIndex_surjective line 43
7. def OAI.NuclearUltrapower.CuntzModel.shift line 47
8. theorem OAI.NuclearUltrapower.CuntzModel.shift_single line 49
9. theorem OAI.NuclearUltrapower.CuntzModel.shift_adjoint_apply line 54
10. theorem OAI.NuclearUltrapower.CuntzModel.shift_adjoint_single_same line 57
11. theorem OAI.NuclearUltrapower.CuntzModel.shift_adjoint_single_ne line 63
12. theorem OAI.NuclearUltrapower.CuntzModel.relations line 70
13. instance OAI.NuclearUltrapower.CuntzModel.(instance at line 87) line 87
14. abbrev OAI.NuclearUltrapower.CuntzPolynomial.Letter line 102
15. abbrev OAI.NuclearUltrapower.CuntzPolynomial.Word line 103
16. def OAI.NuclearUltrapower.CuntzPolynomial.flip line 105
17. theorem OAI.NuclearUltrapower.CuntzPolynomial.flip_flip line 106
18. instance OAI.NuclearUltrapower.CuntzPolynomial.(instance at line 110) line 110
19. theorem OAI.NuclearUltrapower.CuntzPolynomial.star_word_of line 111
20. instance OAI.NuclearUltrapower.CuntzPolynomial.(instance at line 112) line 112
21. instance OAI.NuclearUltrapower.CuntzPolynomial.(instance at line 117) line 117
22. abbrev OAI.NuclearUltrapower.CuntzPolynomial.Poly line 124
23. def OAI.NuclearUltrapower.CuntzPolynomial.involutionAdd line 126
24. instance OAI.NuclearUltrapower.CuntzPolynomial.(instance at line 131) line 131
25. theorem OAI.NuclearUltrapower.CuntzPolynomial.star_single line 132
26. instance OAI.NuclearUltrapower.CuntzPolynomial.(instance at line 136) line 136
27. instance OAI.NuclearUltrapower.CuntzPolynomial.(instance at line 144) line 144
28. instance OAI.NuclearUltrapower.CuntzPolynomial.(instance at line 146) line 146
29. instance OAI.NuclearUltrapower.CuntzPolynomial.(instance at line 156) line 156
30. def OAI.NuclearUltrapower.CuntzPolynomial.evalLetter line 170
31. theorem OAI.NuclearUltrapower.CuntzPolynomial.evalLetter_flip line 171
32. def OAI.NuclearUltrapower.CuntzPolynomial.evalWord line 176
33. theorem OAI.NuclearUltrapower.CuntzPolynomial.evalWord_of line 177
34. theorem OAI.NuclearUltrapower.CuntzPolynomial.evalWord_star line 179
35. def OAI.NuclearUltrapower.CuntzPolynomial.evaluate line 185
36. theorem OAI.NuclearUltrapower.CuntzPolynomial.evaluate_single line 195
37. def OAI.NuclearUltrapower.CuntzPolynomial.generator line 199
38. theorem OAI.NuclearUltrapower.CuntzPolynomial.evaluate_generator line 200
39. theorem OAI.NuclearUltrapower.CuntzPolynomial.evalLetter_norm_le line 203
40. theorem OAI.NuclearUltrapower.CuntzPolynomial.evalWord_norm_le line 214
41. def OAI.NuclearUltrapower.CuntzPolynomial.modelNormSet line 238

    Source documentation

    The possible operator norms in all unital models of the Cuntz relations.

    def modelNormSet (x : Poly) : Set ℝ :=
    …

    Mentions: OAI.NuclearUltrapower.CuntzPolynomial.Poly

42. theorem OAI.NuclearUltrapower.CuntzPolynomial.modelNormSet_nonempty line 241
43. theorem OAI.NuclearUltrapower.CuntzPolynomial.models_bounded line 246

    Source documentation

    Every finite star-polynomial is bounded uniformly over ALL models.

    theorem models_bounded (x : Poly) :
        ∃ M : ℝ, 0 ≤ M ∧ ∀ (D : Type) [CStarAlgebra D] (ρ : Fin 2 → D) (_ : CuntzTwoRelations ρ), ‖evaluate ρ x‖ ≤ M := by
    …

    Mentions: OAI.NuclearUltrapower.CuntzPolynomial.Poly, OAI.NuclearUltrapower.CuntzTwoRelations, OAI.NuclearUltrapower.CuntzPolynomial.evaluate

44. theorem OAI.NuclearUltrapower.CuntzPolynomial.modelNormSet_bdd line 268
45. def OAI.NuclearUltrapower.CuntzPolynomial.universalNorm line 275

    Source documentation

    The universal C*-seminorm over all Cuntz models.

    def universalNorm (x : Poly) : ℝ := sSup (modelNormSet x)

    Mentions: OAI.NuclearUltrapower.CuntzPolynomial.Poly, OAI.NuclearUltrapower.CuntzPolynomial.modelNormSet

46. theorem OAI.NuclearUltrapower.CuntzPolynomial.model_norm_le line 277
47. theorem OAI.NuclearUltrapower.CuntzPolynomial.universalNorm_le line 281
48. theorem OAI.NuclearUltrapower.CuntzPolynomial.universalNorm_nonneg line 288
49. theorem OAI.NuclearUltrapower.CuntzPolynomial.universalNorm_zero line 292
50. def OAI.NuclearUltrapower.CuntzPolynomial.universalSeminorm line 299

    Source documentation

    The universal model supremum is a submultiplicative seminorm.

    def universalSeminorm : RingSeminorm Poly where
    …

    Mentions: OAI.NuclearUltrapower.CuntzPolynomial.Poly

51. instance OAI.NuclearUltrapower.CuntzPolynomial.(instance at line 325) line 325
52. theorem OAI.NuclearUltrapower.CuntzPolynomial.norm_eq_universalNorm line 327
53. instance OAI.NuclearUltrapower.CuntzPolynomial.(instance at line 329) line 329
54. instance OAI.NuclearUltrapower.CuntzPolynomial.(instance at line 335) line 335
55. theorem OAI.NuclearUltrapower.CuntzPolynomial.norm_mul_self_le line 343

    Source documentation

    C*-identity at the seminorm level, which survives separated completion.

    theorem norm_mul_self_le (x : Poly) : ‖x‖ * ‖x‖ ≤ ‖star x * x‖ := by
    …

    Mentions: OAI.NuclearUltrapower.CuntzPolynomial.Poly

56. theorem OAI.NuclearUltrapower.CuntzPolynomial.evaluate_continuous line 353

    Source documentation

    Every model evaluation is contractive for the universal seminorm.

    theorem evaluate_continuous {D : Type} [CStarAlgebra D] (ρ : Fin 2 → D) (hρ : CuntzTwoRelations ρ) :
        Continuous (evaluate ρ) := by
    …

    Mentions: OAI.NuclearUltrapower.CuntzTwoRelations, OAI.NuclearUltrapower.CuntzPolynomial.evaluate

57. def OAI.NuclearUltrapower.CuntzUniversal.Algebra line 366

    Source documentation

    The universal completion is separated; Cuntz relations vanish in its norm.

    def Algebra := Completion Poly

58. instance OAI.NuclearUltrapower.CuntzUniversal.(instance at line 367) line 367
59. def OAI.NuclearUltrapower.CuntzUniversal.inclusion line 369
60. def OAI.NuclearUltrapower.CuntzUniversal.generator line 370
61. def OAI.NuclearUltrapower.CuntzUniversal.modelMap line 372
62. theorem OAI.NuclearUltrapower.CuntzUniversal.modelMap_coe line 375
63. theorem OAI.NuclearUltrapower.CuntzUniversal.modelMap_generator line 379
64. theorem OAI.NuclearUltrapower.CuntzUniversal.inclusion_eq_of_models line 384

    Source documentation

    Seminorm-zero relations become literal equalities in the separated completion.

    theorem inclusion_eq_of_models (x y : Poly)
        (h : ∀ (D : Type) [CStarAlgebra D] (r : Fin 2 → D), CuntzTwoRelations r →
          evaluate r x = evaluate r y) : inclusion x = inclusion y := by
    …

    Mentions: OAI.NuclearUltrapower.CuntzTwoRelations, OAI.NuclearUltrapower.CuntzUniversal.inclusion

65. theorem OAI.NuclearUltrapower.CuntzUniversal.relations line 397
66. instance OAI.NuclearUltrapower.CuntzUniversal.(instance at line 412) line 412
67. theorem OAI.NuclearUltrapower.CuntzUniversal.modelMap_unique line 419

    Source documentation

    Values on the two generators determine all continuous model maps.

    theorem modelMap_unique {D : Type} [CStarAlgebra D] (r : Fin 2 → D)
        (hr : CuntzTwoRelations r) (φ : Algebra →⋆ₐ[ℂ] D)
        (hφ : ∀ i, φ (generator i) = r i) : φ = modelMap r hr := by
    …

    Mentions: OAI.NuclearUltrapower.CuntzTwoRelations, OAI.NuclearUltrapower.CuntzUniversal.Algebra, OAI.NuclearUltrapower.CuntzUniversal.generator, OAI.NuclearUltrapower.CuntzUniversal.modelMap

68. def OAI.NuclearUltrapower.CuntzUniversal.bundled line 452
69. theorem OAI.NuclearUltrapower.CuntzUniversal.universal line 454