OAI/Analysis/FreeEntropy/TracialRealization.lean

GitHub source file

84 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FiniteEntropySeparation.commute_add_star_of_boundary line 11
  2. theorem OAI.FiniteEntropySeparation.LabelHilbert.lift_id line 26
  3. theorem OAI.FiniteEntropySeparation.LabelHilbert.lift_inverse line 33
  4. def OAI.FiniteEntropySeparation.LabelHilbert.keepLinear line 51
  5. def OAI.FiniteEntropySeparation.LabelHilbert.keep line 66
  6. theorem OAI.FiniteEntropySeparation.LabelHilbert.keep_apply line 76
  7. theorem OAI.FiniteEntropySeparation.LabelHilbert.keep_single line 79
  8. theorem OAI.FiniteEntropySeparation.LabelHilbert.star_keep line 88
  9. theorem OAI.FiniteEntropySeparation.FreeTensor.leftG_one line 103
  10. theorem OAI.FiniteEntropySeparation.FreeTensor.leftG_mul line 108
  11. theorem OAI.FiniteEntropySeparation.FreeTensor.unitaryG_one line 112
  12. theorem OAI.FiniteEntropySeparation.FreeTensor.unitaryG_mul line 120
  13. theorem OAI.FiniteEntropySeparation.FreeTensor.star_unitaryG line 127
  14. theorem OAI.FiniteEntropySeparation.FreeTensor.star_rightUnitaryG line 133
  15. theorem OAI.FiniteEntropySeparation.FreeTensor.unitaryG_commutes_rightCreationB line 139
  16. theorem OAI.FiniteEntropySeparation.FreeTensor.unitaryG_commutes_rightCreationN line 143
  17. theorem OAI.FiniteEntropySeparation.FreeTensor.creationB_commutes_rightUnitaryG line 147
  18. theorem OAI.FiniteEntropySeparation.FreeTensor.creationN_commutes_rightUnitaryG line 151
  19. theorem OAI.FiniteEntropySeparation.FreeTensor.unitaryG_commutes_rightUnitaryG line 155
  20. theorem OAI.FiniteEntropySeparation.FreeTensor.unitaryG_commutes_rightAnnihilationB line 159
  21. theorem OAI.FiniteEntropySeparation.FreeTensor.unitaryG_commutes_rightAnnihilationN line 164
  22. theorem OAI.FiniteEntropySeparation.FreeTensor.annihilationB_commutes_rightUnitaryG line 169
  23. theorem OAI.FiniteEntropySeparation.FreeTensor.annihilationN_commutes_rightUnitaryG line 174
  24. def OAI.FiniteEntropySeparation.FreeTensor.signalBoundary line 179
  25. def OAI.FiniteEntropySeparation.FreeTensor.vacuumBoundary line 182
  26. theorem OAI.FiniteEntropySeparation.FreeTensor.signalBoundary_single line 186
  27. theorem OAI.FiniteEntropySeparation.FreeTensor.vacuumBoundary_single line 191
  28. theorem OAI.FiniteEntropySeparation.FreeTensor.rightAnnihilationN_creationN line 195
  29. theorem OAI.FiniteEntropySeparation.FreeTensor.rightAnnihilationB_creationB_atom line 224
  30. theorem OAI.FiniteEntropySeparation.FreeTensor.rightAnnihilationB_creationB_append line 244
  31. theorem OAI.FiniteEntropySeparation.FreeTensor.rightAnnihilationB_creationB line 258
  32. def OAI.FiniteEntropySeparation.FreeTensor.semicircularB line 277
  33. def OAI.FiniteEntropySeparation.FreeTensor.semicircularN line 278
  34. def OAI.FiniteEntropySeparation.FreeTensor.rightSemicircularB line 279
  35. def OAI.FiniteEntropySeparation.FreeTensor.rightSemicircularN line 281
  36. theorem OAI.FiniteEntropySeparation.FreeTensor.star_semicircularB line 285
  37. theorem OAI.FiniteEntropySeparation.FreeTensor.star_semicircularN line 288
  38. theorem OAI.FiniteEntropySeparation.FreeTensor.star_rightSemicircularB line 291
  39. theorem OAI.FiniteEntropySeparation.FreeTensor.star_rightSemicircularN line 294
  40. theorem OAI.FiniteEntropySeparation.FreeTensor.semicircularB_commutes_rightB line 298
  41. theorem OAI.FiniteEntropySeparation.FreeTensor.semicircularN_commutes_rightN line 305
  42. theorem OAI.FiniteEntropySeparation.FreeTensor.semicircularB_commutes_rightN line 312
  43. theorem OAI.FiniteEntropySeparation.FreeTensor.semicircularN_commutes_rightB line 321
  44. theorem OAI.FiniteEntropySeparation.FreeTensor.semicircularB_commutes_rightG line 330
  45. theorem OAI.FiniteEntropySeparation.FreeTensor.semicircularN_commutes_rightG line 334
  46. theorem OAI.FiniteEntropySeparation.FreeTensor.unitaryG_commutes_rightB line 338
  47. theorem OAI.FiniteEntropySeparation.FreeTensor.unitaryG_commutes_rightN line 342
  48. abbrev OAI.FiniteEntropySeparation.FreeTensor.Generator line 346
  49. def OAI.FiniteEntropySeparation.FreeTensor.leftGenerator line 348
  50. def OAI.FiniteEntropySeparation.FreeTensor.rightGenerator line 353
  51. def OAI.FiniteEntropySeparation.FreeTensor.inverseGenerator line 358
  52. theorem OAI.FiniteEntropySeparation.FreeTensor.star_leftGenerator line 363
  53. theorem OAI.FiniteEntropySeparation.FreeTensor.star_rightGenerator line 367
  54. theorem OAI.FiniteEntropySeparation.FreeTensor.generators_commute line 371
  55. def OAI.FiniteEntropySeparation.FreeTensor.algebra line 384
  56. theorem OAI.FiniteEntropySeparation.FreeTensor.mem_algebra_iff line 389
  57. theorem OAI.FiniteEntropySeparation.FreeTensor.leftGenerator_mem line 399
  58. def OAI.FiniteEntropySeparation.FreeTensor.rightWick line 402
  59. theorem OAI.FiniteEntropySeparation.FreeTensor.commute_rightWick line 413
  60. theorem OAI.FiniteEntropySeparation.FreeTensor.reverse_empty line 441
  61. theorem OAI.FiniteEntropySeparation.FreeTensor.rightUnitaryG_basis_reverse line 444
  62. theorem OAI.FiniteEntropySeparation.FreeTensor.rightSemicircularB_basis_reverse line 448
  63. theorem OAI.FiniteEntropySeparation.FreeTensor.rightSemicircularN_basis_reverse line 456
  64. theorem OAI.FiniteEntropySeparation.FreeTensor.rightWick_vacuum line 464
  65. theorem OAI.FiniteEntropySeparation.FreeTensor.inverseGenerator_involutive line 487
  66. theorem OAI.FiniteEntropySeparation.FreeTensor.semicircularB_basis line 492
  67. theorem OAI.FiniteEntropySeparation.FreeTensor.semicircularN_basis line 497
  68. theorem OAI.FiniteEntropySeparation.FreeTensor.unitaryG_basis line 502
  69. theorem OAI.FiniteEntropySeparation.FreeTensor.adjoint_rightGenerator_vacuum line 505
  70. theorem OAI.FiniteEntropySeparation.FreeTensor.adjoint_right_mul_vacuum line 516
  71. theorem OAI.FiniteEntropySeparation.FreeTensor.adjoint_rightB_mul_vacuum line 524
  72. theorem OAI.FiniteEntropySeparation.FreeTensor.adjoint_rightN_mul_vacuum line 529
  73. theorem OAI.FiniteEntropySeparation.FreeTensor.adjoint_rightG_mul_vacuum line 534
  74. theorem OAI.FiniteEntropySeparation.FreeTensor.rightWick_commutesLeft line 539
  75. theorem OAI.FiniteEntropySeparation.FreeTensor.adjoint_rightWick_vacuum line 543
  76. theorem OAI.FiniteEntropySeparation.FreeTensor.vacuum_separating line 577
  77. theorem OAI.FiniteEntropySeparation.FreeTensor.adjoint_vacuum_coefficient line 591
  78. theorem OAI.FiniteEntropySeparation.FreeTensor.vacuum_product_formula line 609
  79. theorem OAI.FiniteEntropySeparation.FreeTensor.vacuum_tracial line 620
  80. def OAI.FiniteEntropySeparation.FreeTensor.tracialVector line 633
  81. theorem OAI.FiniteEntropySeparation.FreeTensor.semicircularB_mem line 640
  82. theorem OAI.FiniteEntropySeparation.FreeTensor.semicircularN_mem line 642
  83. theorem OAI.FiniteEntropySeparation.FreeTensor.unitaryG_mem line 644
  84. theorem OAI.FiniteEntropySeparation.FreeTensor.trace_unitaryG line 647