OAI/Analysis/FreeWords/FreeWordCore.lean

GitHub source file

94 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KKFreeWords.ScalarFree line 15
  2. def OAI.KKFreeWords.FaithfulTracial line 21
  3. structure OAI.KKFreeWords.FreePartitions line 25
  4. def OAI.KKFreeWords.wordSum line 35
  5. def OAI.KKFreeWords.wordValue line 43
  6. def OAI.KKFreeWords.adjointWord line 45
  7. def OAI.KKFreeWords.Reduced line 48
  8. theorem OAI.KKFreeWords.wordValue_nil line 53
  9. theorem OAI.KKFreeWords.wordValue_cons line 56
  10. theorem OAI.KKFreeWords.wordValue_append line 60
  11. theorem OAI.KKFreeWords.adjointWord_nil line 65
  12. theorem OAI.KKFreeWords.adjointWord_cons line 68
  13. theorem OAI.KKFreeWords.wordValue_adjointWord line 73
  14. theorem OAI.KKFreeWords.Reduced.tail line 80
  15. theorem OAI.KKFreeWords.Reduced.head line 85
  16. theorem OAI.KKFreeWords.Reduced.adjointWord line 89
  17. theorem OAI.KKFreeWords.Reduced.trace_zero line 102
  18. theorem OAI.KKFreeWords.chain_iff_indices line 107
  19. theorem OAI.KKFreeWords.adjointWord_indices line 112
  20. theorem OAI.KKFreeWords.chain_junction line 117
  21. theorem OAI.KKFreeWords.chain_distinct_junction line 130
  22. theorem OAI.KKFreeWords.trace_centered_junction line 144
  23. theorem OAI.KKFreeWords.trace_distinct_junction line 162
  24. theorem OAI.KKFreeWords.trace_same_junction line 177
  25. theorem OAI.KKFreeWords.trace_reduced_inner line 198
  26. def OAI.KKFreeWords.gnsVector line 230
  27. theorem OAI.KKFreeWords.gnsVector_inner line 233
  28. theorem OAI.KKFreeWords.gnsStarAlgHom_vector line 239
  29. theorem OAI.KKFreeWords.gnsVector_injective line 245
  30. theorem OAI.KKFreeWords.gnsStarAlgHom_injective line 253
  31. theorem OAI.KKFreeWords.gnsStarAlgHom_norm line 261
  32. theorem OAI.KKFreeWords.gnsVector_word_inner line 266
  33. def OAI.KKFreeWords.HeadOutside line 275
  34. theorem OAI.KKFreeWords.headOutside_nil line 279
  35. theorem OAI.KKFreeWords.headOutside_cons line 283
  36. theorem OAI.KKFreeWords.Reduced.cons_of_headOutside line 287
  37. def OAI.KKFreeWords.tailWords line 301
  38. def OAI.KKFreeWords.tailSpace line 305
  39. theorem OAI.KKFreeWords.inner_create_span line 308
  40. theorem OAI.KKFreeWords.inner_create line 336
  41. theorem OAI.KKFreeWords.closedSpan_orthogonal line 355
  42. def OAI.KKFreeWords.reducedWords line 373
  43. def OAI.KKFreeWords.reducedSpace line 376
  44. def OAI.KKFreeWords.headWords line 379
  45. def OAI.KKFreeWords.headSpace line 383
  46. instance OAI.KKFreeWords.reducedSpace_complete line 386
  47. instance OAI.KKFreeWords.headSpace_complete line 389
  48. instance OAI.KKFreeWords.tailSpace_complete line 392
  49. theorem OAI.KKFreeWords.headSpace_orthogonal_tail line 395
  50. theorem OAI.KKFreeWords.headSpace_le_tailSpace line 405
  51. theorem OAI.KKFreeWords.headSpace_le_reducedSpace line 412
  52. theorem OAI.KKFreeWords.tailSpace_le_reducedSpace line 418
  53. theorem OAI.KKFreeWords.reducedVector_mem line 424
  54. theorem OAI.KKFreeWords.vacuum_mem_reducedSpace line 428
  55. theorem OAI.KKFreeWords.headVector_mem line 432
  56. theorem OAI.KKFreeWords.tailVector_mem line 437
  57. theorem OAI.KKFreeWords.head_add_tail_projection line 442
  58. def OAI.KKFreeWords.centerOf line 488
  59. theorem OAI.KKFreeWords.centerOf_mem line 491
  60. theorem OAI.KKFreeWords.centerOf_trace line 495
  61. theorem OAI.KKFreeWords.gnsVector_mul_split line 498
  62. theorem OAI.KKFreeWords.Reduced.tail_headOutside line 505
  63. theorem OAI.KKFreeWords.map_closedSpan_mem line 513
  64. theorem OAI.KKFreeWords.mul_reducedVector_mem line 522
  65. theorem OAI.KKFreeWords.mul_reducedSpace_mem line 543
  66. theorem OAI.KKFreeWords.create_mem_headSpace line 550
  67. theorem OAI.KKFreeWords.commute_projection_of_invariant line 558
  68. theorem OAI.KKFreeWords.copy_commutes_reducedProjection line 574
  69. def OAI.KKFreeWords.reductionAlgebra line 582
  70. theorem OAI.KKFreeWords.mem_reductionAlgebra line 586
  71. instance OAI.KKFreeWords.reductionAlgebra_closed line 592
  72. def OAI.KKFreeWords.compressedHom line 600
  73. theorem OAI.KKFreeWords.compressedHom_injective line 628
  74. theorem OAI.KKFreeWords.norm_compressed line 639
  75. def OAI.KKFreeWords.creationOp line 646
  76. def OAI.KKFreeWords.preservationOp line 649
  77. def OAI.KKFreeWords.letterOp line 652
  78. theorem OAI.KKFreeWords.head_mul_creation line 655
  79. theorem OAI.KKFreeWords.annihilation_mul_head line 661
  80. theorem OAI.KKFreeWords.head_mul_preservation line 667
  81. theorem OAI.KKFreeWords.preservation_mul_head line 671
  82. theorem OAI.KKFreeWords.head_mul_head_zero line 675
  83. theorem OAI.KKFreeWords.letterOp_decomposition line 682
  84. theorem OAI.KKFreeWords.annihilation_mul_creation_zero line 712
  85. theorem OAI.KKFreeWords.preservation_mul_creation_zero line 724
  86. theorem OAI.KKFreeWords.annihilation_mul_preservation_zero line 735
  87. theorem OAI.KKFreeWords.preservation_mul_preservation_zero line 746
  88. def OAI.KKFreeWords.FreePartitions.centered line 761
  89. theorem OAI.KKFreeWords.FreePartitions.centered_star line 764
  90. theorem OAI.KKFreeWords.FreePartitions.centered_mem line 770
  91. theorem OAI.KKFreeWords.FreePartitions.centered_trace line 774
  92. theorem OAI.KKFreeWords.FreePartitions.centered_gram line 779
  93. theorem OAI.KKFreeWords.FreePartitions.inner_create_row line 787
  94. theorem OAI.KKFreeWords.FreePartitions.norm_create_row_sq line 808