OAI/Analysis/InterpolatedFactors/Fock.lean

GitHub source file

155 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.FreeGroupFactorMain.FreeFock.Op line 12
  2. theorem OAI.FreeGroupFactorMain.FreeFock.operator_basis_ext line 15
  3. def OAI.FreeGroupFactorMain.FreeFock.basisEmbedding line 31
  4. theorem OAI.FreeGroupFactorMain.FreeFock.embedding_orthogonal line 36
  5. def OAI.FreeGroupFactorMain.FreeFock.hilbertEmbedding line 44
  6. theorem OAI.FreeGroupFactorMain.FreeFock.hilbertEmbedding_single line 47
  7. abbrev OAI.FreeGroupFactorMain.FreeFock.Fock line 51
  8. abbrev OAI.FreeGroupFactorMain.FreeFock.Operator line 52
  9. def OAI.FreeGroupFactorMain.FreeFock.consEmbedding line 54
  10. def OAI.FreeGroupFactorMain.FreeFock.creation line 56
  11. theorem OAI.FreeGroupFactorMain.FreeFock.creation_single line 58
  12. theorem OAI.FreeGroupFactorMain.FreeFock.creation_norm line 62
  13. theorem OAI.FreeGroupFactorMain.FreeFock.annihilation_single_nil line 65
  14. theorem OAI.FreeGroupFactorMain.FreeFock.annihilation_single_cons line 73
  15. theorem OAI.FreeGroupFactorMain.FreeFock.annihilation_creation line 88
  16. def OAI.FreeGroupFactorMain.FreeFock.semicircular line 97
  17. theorem OAI.FreeGroupFactorMain.FreeFock.semicircular_selfAdjoint line 99
  18. def OAI.FreeGroupFactorMain.FreeFock.vacuum line 103
  19. theorem OAI.FreeGroupFactorMain.FreeFock.semicircular_vacuum line 105
  20. def OAI.FreeGroupFactorMain.FreeFock.vacuumTrace line 109
  21. theorem OAI.FreeGroupFactorMain.FreeFock.vacuumTrace_one line 111
  22. theorem OAI.FreeGroupFactorMain.FreeFock.vacuumTrace_semicircular line 116
  23. theorem OAI.FreeGroupFactorMain.CoordinateProjection.proj_single line 127
  24. theorem OAI.FreeGroupFactorMain.CoordinateProjection.projection line 135
  25. theorem OAI.FreeGroupFactorMain.CoordinateProjection.commute line 142
  26. theorem OAI.FreeGroupFactorMain.CoordinateProjection.commute_embedding line 149
  27. abbrev OAI.FreeGroupFactorMain.WeightedFock.Path line 169
  28. abbrev OAI.FreeGroupFactorMain.WeightedFock.H line 170
  29. abbrev OAI.FreeGroupFactorMain.WeightedFock.Operator line 171
  30. def OAI.FreeGroupFactorMain.WeightedFock.start line 173
  31. def OAI.FreeGroupFactorMain.WeightedFock.prepend line 177
  32. def OAI.FreeGroupFactorMain.WeightedFock.creation line 183
  33. theorem OAI.FreeGroupFactorMain.WeightedFock.creation_single line 186
  34. theorem OAI.FreeGroupFactorMain.WeightedFock.annihilation_single_nil line 190
  35. theorem OAI.FreeGroupFactorMain.WeightedFock.annihilation_single_cons line 198
  36. def OAI.FreeGroupFactorMain.WeightedFock.P line 217
  37. def OAI.FreeGroupFactorMain.WeightedFock.K line 218
  38. theorem OAI.FreeGroupFactorMain.WeightedFock.projection_P line 221
  39. theorem OAI.FreeGroupFactorMain.WeightedFock.projection_K line 222
  40. theorem OAI.FreeGroupFactorMain.WeightedFock.K_commute_P line 223
  41. theorem OAI.FreeGroupFactorMain.WeightedFock.K_commute_creation line 225
  42. theorem OAI.FreeGroupFactorMain.WeightedFock.P_creation_false line 232
  43. def OAI.FreeGroupFactorMain.WeightedFock.S line 237
  44. theorem OAI.FreeGroupFactorMain.WeightedFock.S_selfAdjoint line 241
  45. def OAI.FreeGroupFactorMain.WeightedFock.compressed line 244
  46. theorem OAI.FreeGroupFactorMain.WeightedFock.compressed_formula line 246
  47. theorem OAI.FreeGroupFactorMain.WeightedFock.K_commute_compressed line 255
  48. theorem OAI.FreeGroupFactorMain.WeightedFock.P_single line 271
  49. theorem OAI.FreeGroupFactorMain.WeightedFock.P_nil_true line 286
  50. theorem OAI.FreeGroupFactorMain.WeightedFock.P_nil_false line 289
  51. theorem OAI.FreeGroupFactorMain.WeightedFock.P_cons line 291
  52. theorem OAI.FreeGroupFactorMain.WeightedFock.K_nil_true line 298
  53. theorem OAI.FreeGroupFactorMain.WeightedFock.K_mixed line 301
  54. def OAI.FreeGroupFactorMain.WeightedFock.excursion line 305
  55. theorem OAI.FreeGroupFactorMain.WeightedFock.S_nil line 307
  56. theorem OAI.FreeGroupFactorMain.WeightedFock.S_cons_distinct line 314
  57. theorem OAI.FreeGroupFactorMain.WeightedFock.excursion_start line 323
  58. def OAI.FreeGroupFactorMain.WeightedFock.compressedAlgebra line 334
  59. theorem OAI.FreeGroupFactorMain.WeightedFock.compressed_selfAdjoint line 338
  60. theorem OAI.FreeGroupFactorMain.WeightedFock.K_in_compressedCommutant line 343
  61. theorem OAI.FreeGroupFactorMain.WeightedFock.excursion_not_in_compressedAlgebra line 351
  62. def OAI.FreeGroupFactorMain.WeightedFock.ambientAlgebra line 363
  63. theorem OAI.FreeGroupFactorMain.WeightedFock.P_mem_ambient line 367
  64. theorem OAI.FreeGroupFactorMain.WeightedFock.S_mem_ambient line 371
  65. theorem OAI.FreeGroupFactorMain.WeightedFock.excursion_mem_ambient line 375
  66. theorem OAI.FreeGroupFactorMain.WeightedFock.excursion_in_corner line 384
  67. theorem OAI.FreeGroupFactorMain.WeightedFock.compression_generation_obstruction line 392
  68. def OAI.FreeGroupFactorMain.WeightedFock.appendPath line 405
  69. def OAI.FreeGroupFactorMain.WeightedFock.reverseList line 406
  70. def OAI.FreeGroupFactorMain.WeightedFock.reversePath line 410
  71. theorem OAI.FreeGroupFactorMain.WeightedFock.reverse_nil line 412
  72. theorem OAI.FreeGroupFactorMain.WeightedFock.reverse_cons line 413
  73. theorem OAI.FreeGroupFactorMain.WeightedFock.start_appendPath line 416
  74. theorem OAI.FreeGroupFactorMain.WeightedFock.reverse_append line 421
  75. theorem OAI.FreeGroupFactorMain.WeightedFock.reversePath_involutive line 432
  76. theorem OAI.FreeGroupFactorMain.WeightedFock.end_reverse line 445
  77. theorem OAI.FreeGroupFactorMain.WeightedFock.start_reverse line 451
  78. theorem OAI.FreeGroupFactorMain.WeightedFock.reversePath_reverse line 456
  79. def OAI.FreeGroupFactorMain.WeightedFock.reverseEmbedding line 461
  80. def OAI.FreeGroupFactorMain.WeightedFock.reverseIsometry line 462
  81. def OAI.FreeGroupFactorMain.WeightedFock.reverseOperator line 463
  82. theorem OAI.FreeGroupFactorMain.WeightedFock.reverseOperator_single line 465
  83. theorem OAI.FreeGroupFactorMain.WeightedFock.reverseOperator_square line 469
  84. theorem OAI.FreeGroupFactorMain.WeightedFock.reverseOperator_involutive line 474
  85. def OAI.FreeGroupFactorMain.WeightedFock.reverseEquiv line 477
  86. theorem OAI.FreeGroupFactorMain.WeightedFock.reverseEquiv_apply line 481
  87. theorem OAI.FreeGroupFactorMain.WeightedFock.reverseEquiv_symm_apply line 482
  88. def OAI.FreeGroupFactorMain.WeightedFock.reverseConj line 486
  89. theorem OAI.FreeGroupFactorMain.WeightedFock.reverseConj_apply line 488
  90. def OAI.FreeGroupFactorMain.WeightedFock.appendEmbedding line 493
  91. def OAI.FreeGroupFactorMain.WeightedFock.rightCreation line 502
  92. theorem OAI.FreeGroupFactorMain.WeightedFock.rightCreation_single line 505
  93. theorem OAI.FreeGroupFactorMain.WeightedFock.reverseConj_creation line 509
  94. def OAI.FreeGroupFactorMain.WeightedFock.rightP line 516
  95. theorem OAI.FreeGroupFactorMain.WeightedFock.reverseConj_P line 518
  96. def OAI.FreeGroupFactorMain.WeightedFock.vacuum line 525
  97. theorem OAI.FreeGroupFactorMain.WeightedFock.reverse_vacuum line 528
  98. theorem OAI.FreeGroupFactorMain.WeightedFock.right_creation_commute line 531
  99. theorem OAI.FreeGroupFactorMain.WeightedFock.P_commute_rightCreation line 539
  100. theorem OAI.FreeGroupFactorMain.WeightedFock.rightP_commute_creation line 546
  101. theorem OAI.FreeGroupFactorMain.WeightedFock.P_commute_rightP line 552
  102. def OAI.FreeGroupFactorMain.WeightedFock.vacuumMatrix line 560
  103. theorem OAI.FreeGroupFactorMain.WeightedFock.vacuumMatrix_nil line 563
  104. theorem OAI.FreeGroupFactorMain.WeightedFock.vacuumMatrix_cons line 575
  105. theorem OAI.FreeGroupFactorMain.WeightedFock.star_vacuumMatrix line 580
  106. theorem OAI.FreeGroupFactorMain.WeightedFock.annihilation_rightCreation line 584
  107. def OAI.FreeGroupFactorMain.WeightedFock.C line 610
  108. def OAI.FreeGroupFactorMain.WeightedFock.rightC line 613
  109. theorem OAI.FreeGroupFactorMain.WeightedFock.reverseConj_C line 616
  110. theorem OAI.FreeGroupFactorMain.WeightedFock.S_eq line 619
  111. def OAI.FreeGroupFactorMain.WeightedFock.rightS line 621
  112. theorem OAI.FreeGroupFactorMain.WeightedFock.reverseConj_S line 623
  113. def OAI.FreeGroupFactorMain.WeightedFock.vacuumCorrection line 628
  114. theorem OAI.FreeGroupFactorMain.WeightedFock.vacuumCorrection_selfAdjoint line 634
  115. theorem OAI.FreeGroupFactorMain.WeightedFock.C_commute_rightC line 641
  116. theorem OAI.FreeGroupFactorMain.WeightedFock.C_annihilation_rightC line 648
  117. theorem OAI.FreeGroupFactorMain.WeightedFock.add_star_commute_of_correction line 661
  118. theorem OAI.FreeGroupFactorMain.WeightedFock.S_commute_rightS line 676
  119. theorem OAI.FreeGroupFactorMain.WeightedFock.rightP_projection line 685
  120. theorem OAI.FreeGroupFactorMain.WeightedFock.P_commute_rightS line 687
  121. theorem OAI.FreeGroupFactorMain.WeightedFock.rightP_commute_S line 695
  122. def OAI.FreeGroupFactorMain.WeightedFock.ambientCommutant line 710
  123. def OAI.FreeGroupFactorMain.WeightedFock.Good line 713
  124. theorem OAI.FreeGroupFactorMain.WeightedFock.good_one line 717
  125. theorem OAI.FreeGroupFactorMain.WeightedFock.good_zero line 722
  126. theorem OAI.FreeGroupFactorMain.WeightedFock.good_add line 727
  127. theorem OAI.FreeGroupFactorMain.WeightedFock.good_sub line 733
  128. theorem OAI.FreeGroupFactorMain.WeightedFock.good_smul line 739
  129. theorem OAI.FreeGroupFactorMain.WeightedFock.good_mul line 746
  130. theorem OAI.FreeGroupFactorMain.WeightedFock.reverseConj_vacuum line 755
  131. theorem OAI.FreeGroupFactorMain.WeightedFock.rightP_mem_commutant line 759
  132. theorem OAI.FreeGroupFactorMain.WeightedFock.rightS_mem_commutant line 771
  133. theorem OAI.FreeGroupFactorMain.WeightedFock.good_P line 783
  134. theorem OAI.FreeGroupFactorMain.WeightedFock.good_S line 790
  135. def OAI.FreeGroupFactorMain.WeightedFock.vertex line 798
  136. def OAI.FreeGroupFactorMain.WeightedFock.weight line 800
  137. theorem OAI.FreeGroupFactorMain.WeightedFock.good_vertex line 802
  138. theorem OAI.FreeGroupFactorMain.WeightedFock.weight_ne_zero line 807
  139. theorem OAI.FreeGroupFactorMain.WeightedFock.vertex_single line 810
  140. theorem OAI.FreeGroupFactorMain.WeightedFock.vertex_S_nil line 814
  141. theorem OAI.FreeGroupFactorMain.WeightedFock.S_cons line 822
  142. theorem OAI.FreeGroupFactorMain.WeightedFock.vertex_S_cons line 831
  143. theorem OAI.FreeGroupFactorMain.WeightedFock.vertex_vacuum line 840
  144. theorem OAI.FreeGroupFactorMain.WeightedFock.good_basis line 846
  145. theorem OAI.FreeGroupFactorMain.WeightedFock.good_star line 903
  146. theorem OAI.FreeGroupFactorMain.WeightedFock.good_right_basis line 911
  147. theorem OAI.FreeGroupFactorMain.WeightedFock.ambient_separating line 920
  148. theorem OAI.FreeGroupFactorMain.WeightedFock.ambient_star_vector line 931
  149. def OAI.FreeGroupFactorMain.WeightedFock.vacuumTrace line 950
  150. theorem OAI.FreeGroupFactorMain.WeightedFock.ambient_trace_mul line 952
  151. theorem OAI.FreeGroupFactorMain.WeightedFock.vacuumTrace_star_mul line 977
  152. theorem OAI.FreeGroupFactorMain.WeightedFock.ambient_trace_faithful line 982
  153. theorem OAI.FreeGroupFactorMain.WeightedFock.vacuumTrace_one line 988
  154. theorem OAI.FreeGroupFactorMain.WeightedFock.vacuumTrace_P line 993
  155. theorem OAI.FreeGroupFactorMain.WeightedFock.tracial_compression_generation_obstruction line 998