OAI/Analysis/FreeEntropy/Basic.lean

GitHub source file

186 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FiniteEntropySeparation.trace_zero line 15
  2. theorem OAI.FiniteEntropySeparation.trace_add line 18
  3. theorem OAI.FiniteEntropySeparation.trace_smul line 22
  4. theorem OAI.FiniteEntropySeparation.trace_sum line 26
  5. theorem OAI.FiniteEntropySeparation.ConjugateSystem.unique line 31
  6. theorem OAI.FiniteEntropySeparation.freeFisher_eq_of_conjugate line 47
  7. theorem OAI.FiniteEntropySeparation.trace_one line 56
  8. theorem OAI.FiniteEntropySeparation.wordMoment_nil line 60
  9. theorem OAI.FiniteEntropySeparation.wordVector_mem_polynomialL2 line 64
  10. instance OAI.FiniteEntropySeparation.polynomialL2_complete line 69
  11. def OAI.FiniteEntropySeparation.projectedConjugate line 73
  12. theorem OAI.FiniteEntropySeparation.projectedConjugate_system line 77
  13. theorem OAI.FiniteEntropySeparation.freeFisher_le_testVectors line 88
  14. theorem OAI.FiniteEntropySeparation.conjugate_coordinate_pairing line 98
  15. theorem OAI.FiniteEntropySeparation.conjugate_norm_sq_lower line 104
  16. theorem OAI.FiniteEntropySeparation.freeFisher_lower_covariance line 120
  17. def OAI.FiniteEntropySeparation.vacuumRankOne line 127
  18. def OAI.FiniteEntropySeparation.commutatorKernel line 130
  19. theorem OAI.FiniteEntropySeparation.commutatorKernel_nil line 136
  20. theorem OAI.FiniteEntropySeparation.commutatorKernel_cons line 141
  21. theorem OAI.FiniteEntropySeparation.commutator_word line 155
  22. theorem OAI.FiniteEntropySeparation.trace_vacuumRankOne_product line 169
  23. theorem OAI.FiniteEntropySeparation.trace_commutatorKernel line 175
  24. theorem OAI.FiniteEntropySeparation.commutator_integration_by_parts line 183
  25. theorem OAI.FiniteEntropySeparation.FreeSubalgebras.mono line 195
  26. abbrev OAI.FiniteEntropySeparation.Fock.Space line 206
  27. instance OAI.FiniteEntropySeparation.Fock.space_nontrivial line 208
  28. def OAI.FiniteEntropySeparation.Fock.basisVector line 214
  29. def OAI.FiniteEntropySeparation.Fock.coordinateIsometry line 216
  30. theorem OAI.FiniteEntropySeparation.Fock.coordinateIsometry_apply line 220
  31. theorem OAI.FiniteEntropySeparation.Fock.orthogonal_coordinates line 223
  32. def OAI.FiniteEntropySeparation.Fock.injectionIsometry line 230
  33. theorem OAI.FiniteEntropySeparation.Fock.injectionIsometry_single line 234
  34. def OAI.FiniteEntropySeparation.Fock.creation line 239
  35. def OAI.FiniteEntropySeparation.Fock.rightCreation line 242
  36. theorem OAI.FiniteEntropySeparation.Fock.creation_single line 245
  37. theorem OAI.FiniteEntropySeparation.Fock.rightCreation_single line 249
  38. def OAI.FiniteEntropySeparation.Fock.semicircular line 253
  39. def OAI.FiniteEntropySeparation.Fock.rightSemicircular line 255
  40. theorem OAI.FiniteEntropySeparation.Fock.semicircular_selfAdjoint line 258
  41. theorem OAI.FiniteEntropySeparation.Fock.rightSemicircular_selfAdjoint line 261
  42. theorem OAI.FiniteEntropySeparation.Fock.semicircular_norm_le line 264
  43. theorem OAI.FiniteEntropySeparation.Fock.adjoint_creation_apply line 269
  44. theorem OAI.FiniteEntropySeparation.Fock.adjoint_rightCreation_apply line 274
  45. theorem OAI.FiniteEntropySeparation.Fock.annihilation_single_nil line 279
  46. theorem OAI.FiniteEntropySeparation.Fock.annihilation_single_cons line 285
  47. theorem OAI.FiniteEntropySeparation.Fock.rightAnnihilation_single_nil line 295
  48. theorem OAI.FiniteEntropySeparation.Fock.rightAnnihilation_single_append line 301
  49. theorem OAI.FiniteEntropySeparation.Fock.semicircular_single_nil line 311
  50. theorem OAI.FiniteEntropySeparation.Fock.semicircular_single_cons line 315
  51. theorem OAI.FiniteEntropySeparation.Fock.rightSemicircular_single_nil line 320
  52. theorem OAI.FiniteEntropySeparation.Fock.rightSemicircular_single_append line 324
  53. theorem OAI.FiniteEntropySeparation.Fock.semicircular_commutes_right line 329
  54. def OAI.FiniteEntropySeparation.Fock.rightWick line 361
  55. theorem OAI.FiniteEntropySeparation.Fock.commute_rightWick line 367
  56. theorem OAI.FiniteEntropySeparation.Fock.rightWick_vacuum line 380
  57. theorem OAI.FiniteEntropySeparation.Fock.adjoint_rightWick_vacuum line 391
  58. def OAI.FiniteEntropySeparation.Fock.algebra line 414
  59. theorem OAI.FiniteEntropySeparation.Fock.mem_algebra_iff line 418
  60. theorem OAI.FiniteEntropySeparation.Fock.semicircular_mem line 425
  61. theorem OAI.FiniteEntropySeparation.Fock.vacuum_separating line 428
  62. theorem OAI.FiniteEntropySeparation.Fock.adjoint_vacuum_coefficient line 444
  63. theorem OAI.FiniteEntropySeparation.Fock.vacuum_product_formula line 463
  64. theorem OAI.FiniteEntropySeparation.Fock.vacuum_tracial line 474
  65. def OAI.FiniteEntropySeparation.Fock.tracialVector line 487
  66. def OAI.FiniteEntropySeparation.Fock.vacuumProjection line 494
  67. theorem OAI.FiniteEntropySeparation.Fock.vacuumProjection_single line 497
  68. theorem OAI.FiniteEntropySeparation.Fock.creation_commutes_rightCreation line 504
  69. theorem OAI.FiniteEntropySeparation.Fock.rightAnnihilation_creation line 515
  70. theorem OAI.FiniteEntropySeparation.Fock.rightAnnihilation_semicircular line 537
  71. def OAI.FiniteEntropySeparation.Fock.derivativeKernel line 546
  72. theorem OAI.FiniteEntropySeparation.Fock.derivativeKernel_nil line 552
  73. theorem OAI.FiniteEntropySeparation.Fock.derivativeKernel_cons line 555
  74. theorem OAI.FiniteEntropySeparation.Fock.rightAnnihilation_word line 568
  75. theorem OAI.FiniteEntropySeparation.Fock.trace_projection_product line 580
  76. theorem OAI.FiniteEntropySeparation.Fock.trace_derivativeKernel line 587
  77. theorem OAI.FiniteEntropySeparation.Fock.trace_semicircular_left line 595
  78. theorem OAI.FiniteEntropySeparation.Fock.semicircular_integration_by_parts line 605
  79. theorem OAI.FiniteEntropySeparation.Fock.semicircular_conjugateSystem line 613
  80. theorem OAI.FiniteEntropySeparation.Fock.semicircular_freeFisher line 629
  81. theorem OAI.FiniteEntropySeparation.Fock.semicircular_moment_succ line 634
  82. theorem OAI.FiniteEntropySeparation.Fock.sum_range_double line 652
  83. theorem OAI.FiniteEntropySeparation.Fock.semicircular_moments line 662
  84. def OAI.FiniteEntropySeparation.Fock.wordSpace line 710
  85. def OAI.FiniteEntropySeparation.Fock.startsIn line 713
  86. def OAI.FiniteEntropySeparation.Fock.suffixEmbedding line 716
  87. theorem OAI.FiniteEntropySeparation.Fock.suffixEmbedding_basis line 719
  88. theorem OAI.FiniteEntropySeparation.Fock.basis_mem_wordSpace line 723
  89. theorem OAI.FiniteEntropySeparation.Fock.vacuum_mem_wordSpace line 726
  90. theorem OAI.FiniteEntropySeparation.Fock.semicircular_preserves_wordSpace line 729
  91. theorem OAI.FiniteEntropySeparation.Fock.semicircular_suffix line 750
  92. theorem OAI.FiniteEntropySeparation.Fock.adjoin_suffix line 773
  93. theorem OAI.FiniteEntropySeparation.Fock.centered_wordSpace_suffix line 796
  94. theorem OAI.FiniteEntropySeparation.Fock.trace_eq_vacuum_coefficient line 823
  95. theorem OAI.FiniteEntropySeparation.Fock.centered_adjoin_basis line 827
  96. theorem OAI.FiniteEntropySeparation.Fock.centered_adjoin_startsIn line 837
  97. theorem OAI.FiniteEntropySeparation.Fock.startsIn_vacuum_zero line 853
  98. theorem OAI.FiniteEntropySeparation.Fock.alternating_product_starts line 862
  99. theorem OAI.FiniteEntropySeparation.Fock.free_grouped_semicircular line 886
  100. theorem OAI.FiniteEntropySeparation.Fock.free_semicircular line 894
  101. theorem OAI.FiniteEntropySeparation.Fock.freeStandardNoise line 899
  102. theorem OAI.FiniteEntropySeparation.Fock.rightAnnihilation_adjoin line 928
  103. theorem OAI.FiniteEntropySeparation.Fock.heat_freeFisher_le line 941
  104. abbrev OAI.FiniteEntropySeparation.LabelHilbert.Space line 992
  105. def OAI.FiniteEntropySeparation.LabelHilbert.basis line 994
  106. def OAI.FiniteEntropySeparation.LabelHilbert.coordinateIsometry line 996
  107. theorem OAI.FiniteEntropySeparation.LabelHilbert.orthogonal_coordinates line 1000
  108. def OAI.FiniteEntropySeparation.LabelHilbert.lift line 1009
  109. theorem OAI.FiniteEntropySeparation.LabelHilbert.lift_single line 1012
  110. theorem OAI.FiniteEntropySeparation.LabelHilbert.lift_basis line 1016
  111. theorem OAI.FiniteEntropySeparation.LabelHilbert.adjoint_apply line 1019
  112. theorem OAI.FiniteEntropySeparation.LabelHilbert.adjoint_single_of_inverse line 1024
  113. theorem OAI.FiniteEntropySeparation.LabelHilbert.lift_mul line 1044
  114. theorem OAI.FiniteEntropySeparation.LabelHilbert.lift_commute line 1053
  115. abbrev OAI.FiniteEntropySeparation.FreeTensor.Atom line 1064
  116. abbrev OAI.FiniteEntropySeparation.FreeTensor.Word line 1065
  117. def OAI.FiniteEntropySeparation.FreeTensor.empty line 1067
  118. def OAI.FiniteEntropySeparation.FreeTensor.push line 1068
  119. def OAI.FiniteEntropySeparation.FreeTensor.append line 1070
  120. def OAI.FiniteEntropySeparation.FreeTensor.reverseAtom line 1072
  121. theorem OAI.FiniteEntropySeparation.FreeTensor.reverseAtom_involutive line 1074
  122. def OAI.FiniteEntropySeparation.FreeTensor.reverseAux line 1077
  123. def OAI.FiniteEntropySeparation.FreeTensor.reverse line 1080
  124. theorem OAI.FiniteEntropySeparation.FreeTensor.reverse_nil line 1082
  125. theorem OAI.FiniteEntropySeparation.FreeTensor.reverse_push line 1084
  126. theorem OAI.FiniteEntropySeparation.FreeTensor.push_append line 1088
  127. theorem OAI.FiniteEntropySeparation.FreeTensor.reverse_append line 1091
  128. theorem OAI.FiniteEntropySeparation.FreeTensor.reverse_involutive line 1102
  129. def OAI.FiniteEntropySeparation.FreeTensor.leftB line 1112
  130. def OAI.FiniteEntropySeparation.FreeTensor.leftN line 1113
  131. def OAI.FiniteEntropySeparation.FreeTensor.leftG line 1114
  132. def OAI.FiniteEntropySeparation.FreeTensor.rightB line 1115
  133. def OAI.FiniteEntropySeparation.FreeTensor.rightN line 1116
  134. def OAI.FiniteEntropySeparation.FreeTensor.rightG line 1117
  135. theorem OAI.FiniteEntropySeparation.FreeTensor.leftB_injective line 1120
  136. theorem OAI.FiniteEntropySeparation.FreeTensor.leftN_injective line 1123
  137. theorem OAI.FiniteEntropySeparation.FreeTensor.leftG_injective line 1126
  138. theorem OAI.FiniteEntropySeparation.FreeTensor.reverse_injective line 1129
  139. theorem OAI.FiniteEntropySeparation.FreeTensor.rightB_injective line 1131
  140. theorem OAI.FiniteEntropySeparation.FreeTensor.rightN_injective line 1133
  141. theorem OAI.FiniteEntropySeparation.FreeTensor.rightG_injective line 1135
  142. theorem OAI.FiniteEntropySeparation.FreeTensor.rightB_nil line 1138
  143. theorem OAI.FiniteEntropySeparation.FreeTensor.rightB_push line 1141
  144. theorem OAI.FiniteEntropySeparation.FreeTensor.rightN_eq_append line 1147
  145. theorem OAI.FiniteEntropySeparation.FreeTensor.rightG_nil line 1152
  146. theorem OAI.FiniteEntropySeparation.FreeTensor.rightG_push line 1155
  147. theorem OAI.FiniteEntropySeparation.FreeTensor.leftB_rightB line 1162
  148. theorem OAI.FiniteEntropySeparation.FreeTensor.leftN_rightB line 1173
  149. theorem OAI.FiniteEntropySeparation.FreeTensor.leftG_rightB line 1177
  150. theorem OAI.FiniteEntropySeparation.FreeTensor.leftB_rightN line 1188
  151. theorem OAI.FiniteEntropySeparation.FreeTensor.leftN_rightN line 1193
  152. theorem OAI.FiniteEntropySeparation.FreeTensor.leftG_rightN line 1198
  153. theorem OAI.FiniteEntropySeparation.FreeTensor.leftB_rightG line 1203
  154. theorem OAI.FiniteEntropySeparation.FreeTensor.leftN_rightG line 1214
  155. theorem OAI.FiniteEntropySeparation.FreeTensor.leftG_rightG line 1218
  156. abbrev OAI.FiniteEntropySeparation.FreeTensor.Space line 1232
  157. def OAI.FiniteEntropySeparation.FreeTensor.basis line 1233
  158. def OAI.FiniteEntropySeparation.FreeTensor.creationB line 1235
  159. def OAI.FiniteEntropySeparation.FreeTensor.creationN line 1237
  160. def OAI.FiniteEntropySeparation.FreeTensor.unitaryG line 1239
  161. def OAI.FiniteEntropySeparation.FreeTensor.rightCreationB line 1241
  162. def OAI.FiniteEntropySeparation.FreeTensor.rightCreationN line 1243
  163. def OAI.FiniteEntropySeparation.FreeTensor.rightUnitaryG line 1245
  164. theorem OAI.FiniteEntropySeparation.FreeTensor.creationB_single line 1249
  165. theorem OAI.FiniteEntropySeparation.FreeTensor.creationN_single line 1252
  166. theorem OAI.FiniteEntropySeparation.FreeTensor.unitaryG_single line 1255
  167. theorem OAI.FiniteEntropySeparation.FreeTensor.rightCreationB_single line 1258
  168. theorem OAI.FiniteEntropySeparation.FreeTensor.rightCreationN_single line 1261
  169. theorem OAI.FiniteEntropySeparation.FreeTensor.rightUnitaryG_single line 1264
  170. def OAI.FiniteEntropySeparation.FreeTensor.removeB line 1268
  171. def OAI.FiniteEntropySeparation.FreeTensor.removeN line 1273
  172. theorem OAI.FiniteEntropySeparation.FreeTensor.removeB_spec line 1280
  173. theorem OAI.FiniteEntropySeparation.FreeTensor.removeN_spec line 1290
  174. theorem OAI.FiniteEntropySeparation.FreeTensor.annihilationB_single line 1305
  175. theorem OAI.FiniteEntropySeparation.FreeTensor.annihilationN_single line 1309
  176. theorem OAI.FiniteEntropySeparation.FreeTensor.right_remove_spec line 1315
  177. theorem OAI.FiniteEntropySeparation.FreeTensor.rightAnnihilationB_single line 1330
  178. theorem OAI.FiniteEntropySeparation.FreeTensor.rightAnnihilationN_single line 1334
  179. theorem OAI.FiniteEntropySeparation.FreeTensor.rightAnnihilationN_atom line 1339
  180. theorem OAI.FiniteEntropySeparation.FreeTensor.rightAnnihilationN_append line 1348
  181. theorem OAI.FiniteEntropySeparation.FreeTensor.rightAnnihilationB_atom_nil line 1360
  182. theorem OAI.FiniteEntropySeparation.FreeTensor.rightAnnihilationB_atom_append line 1365
  183. theorem OAI.FiniteEntropySeparation.FreeTensor.rightAnnihilationB_append_nil line 1371
  184. theorem OAI.FiniteEntropySeparation.FreeTensor.rightAnnihilationB_append_append line 1377
  185. theorem OAI.FiniteEntropySeparation.FreeTensor.creationB_commutes_rightAnnihilationN line 1387
  186. theorem OAI.FiniteEntropySeparation.FreeTensor.creationN_commutes_rightAnnihilationB line 1408