OAI/Analysis/Naimark/CAR.lean

GitHub source file

73 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.NaimarkZFC.CARStage line 11
  2. def OAI.NaimarkZFC.carStageCStarAux line 15
  3. instance OAI.NaimarkZFC.carStageCStar line 22
  4. instance OAI.NaimarkZFC.carStagePartialOrder line 24
  5. instance OAI.NaimarkZFC.carStageStarOrder line 26
  6. instance OAI.NaimarkZFC.carStageNontrivial line 29
  7. instance OAI.NaimarkZFC.carStageSimple line 35
  8. def OAI.NaimarkZFC.matrixScalarHom line 42
  9. theorem OAI.NaimarkZFC.matrixScalarHom_entry line 61
  10. theorem OAI.NaimarkZFC.matrixScalarHom_injective line 64
  11. theorem OAI.NaimarkZFC.matrixScalarHom_isometry line 70
  12. def OAI.NaimarkZFC.carStep line 75
  13. def OAI.NaimarkZFC.carBond line 77
  14. theorem OAI.NaimarkZFC.carBond_self line 80
  15. theorem OAI.NaimarkZFC.carBond_succ line 83
  16. theorem OAI.NaimarkZFC.carBond_comp line 87
  17. instance OAI.NaimarkZFC.carDirected line 94
  18. theorem OAI.NaimarkZFC.carBond_isometry line 99
  19. instance OAI.NaimarkZFC.carIsometricSystem line 108
  20. abbrev OAI.NaimarkZFC.CAR line 110
  21. abbrev OAI.NaimarkZFC.carInclude line 112
  22. theorem OAI.NaimarkZFC.carInclude_isometry line 115
  23. instance OAI.NaimarkZFC.carNontrivial line 118
  24. instance OAI.NaimarkZFC.carOrder line 120
  25. instance OAI.NaimarkZFC.carStarOrder line 121
  26. instance OAI.NaimarkZFC.carStageFinite line 123
  27. theorem OAI.NaimarkZFC.carStage_finrank line 130
  28. theorem OAI.NaimarkZFC.carSimple line 139
  29. instance OAI.NaimarkZFC.carSeparable line 146
  30. theorem OAI.NaimarkZFC.carInfiniteDimensional line 154
  31. theorem OAI.NaimarkZFC.complex_identity_isState line 167
  32. def OAI.NaimarkZFC.carStageTrace line 173
  33. theorem OAI.NaimarkZFC.carStageTrace_zero line 177
  34. theorem OAI.NaimarkZFC.carStageTrace_succ line 179
  35. theorem OAI.NaimarkZFC.carStageTrace_tracial line 182
  36. theorem OAI.NaimarkZFC.carStageTrace_step line 188
  37. theorem OAI.NaimarkZFC.carStageTrace_compatible line 194
  38. def OAI.NaimarkZFC.carTrace line 200
  39. theorem OAI.NaimarkZFC.carTrace_isState line 203
  40. theorem OAI.NaimarkZFC.carTrace_stage line 205
  41. theorem OAI.NaimarkZFC.carTrace_tracial line 208
  42. theorem OAI.NaimarkZFC.carTrace_faithful line 211
  43. def OAI.NaimarkZFC.carStageVector line 214
  44. theorem OAI.NaimarkZFC.carStageVector_step line 218
  45. theorem OAI.NaimarkZFC.carStageVector_compatible line 222
  46. def OAI.NaimarkZFC.carVector line 228
  47. theorem OAI.NaimarkZFC.carVector_isState line 231
  48. theorem OAI.NaimarkZFC.carVector_stage line 233
  49. def OAI.NaimarkZFC.carStagePeak line 238
  50. theorem OAI.NaimarkZFC.carStagePeak_projection line 242
  51. theorem OAI.NaimarkZFC.carStagePeak_compress line 247
  52. theorem OAI.NaimarkZFC.carStageVector_peak line 260
  53. theorem OAI.NaimarkZFC.carStageTrace_peak line 267
  54. theorem OAI.NaimarkZFC.carStagePeak_bond line 278
  55. def OAI.NaimarkZFC.carPeak line 289
  56. theorem OAI.NaimarkZFC.carPeak_zero line 291
  57. theorem OAI.NaimarkZFC.carPeak_projection line 293
  58. theorem OAI.NaimarkZFC.carPeak_antitone line 296
  59. theorem OAI.NaimarkZFC.carVector_peak line 307
  60. theorem OAI.NaimarkZFC.carTrace_peak line 310
  61. theorem OAI.NaimarkZFC.carPeak_unique line 313
  62. theorem OAI.NaimarkZFC.carPeak_peaks line 328
  63. theorem OAI.NaimarkZFC.carVector_isPure line 331
  64. theorem OAI.NaimarkZFC.matrixScalar_eq_sum_single line 337
  65. theorem OAI.NaimarkZFC.trace_two_corners line 342
  66. theorem OAI.NaimarkZFC.trace_matrix_corner line 348
  67. theorem OAI.NaimarkZFC.carStage_normalizedTrace_peak line 358
  68. theorem OAI.NaimarkZFC.carPeak_ambientTrace line 386
  69. theorem OAI.NaimarkZFC.carPeak_autTrace line 397
  70. theorem OAI.NaimarkZFC.Peaks.mapEquiv line 411
  71. theorem OAI.NaimarkZFC.complexInvTwoPow_re line 427
  72. theorem OAI.NaimarkZFC.homogeneousCARPeak_peaks line 440
  73. def OAI.NaimarkZFC.homogeneousCARPeakPair line 445