OAI/MathematicalPhysics/Heisenberg/LocalAlgebra.lean

GitHub source file

75 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.Heisenberg.quasiLocalNormedRing line 11
  2. instance OAI.Heisenberg.quasiLocalStarRing line 14
  3. instance OAI.Heisenberg.quasiLocalNormedAlgebra line 17
  4. instance OAI.Heisenberg.quasiLocalAddCommGroup line 20
  5. instance OAI.Heisenberg.quasiLocalAddCommMonoid line 23
  6. instance OAI.Heisenberg.quasiLocalAddMonoid line 26
  7. instance OAI.Heisenberg.quasiLocalAddZeroClass line 29
  8. instance OAI.Heisenberg.quasiLocalAddCommMagma line 32
  9. instance OAI.Heisenberg.quasiLocalStarMul line 35
  10. instance OAI.Heisenberg.quasiLocalModule line 38
  11. theorem OAI.Heisenberg.matrixUnit_mul_same line 41
  12. theorem OAI.Heisenberg.matrixUnit_diagonal_sum line 54
  13. theorem OAI.Heisenberg.matrixUnits_commute line 63
  14. theorem OAI.Heisenberg.localUnit_mul_same line 75
  15. theorem OAI.Heisenberg.localUnit_diagonal_sum line 84
  16. theorem OAI.Heisenberg.localUnits_commute line 92
  17. theorem OAI.Heisenberg.star_l2Projection line 99
  18. theorem OAI.Heisenberg.star_l2Reindex line 110
  19. theorem OAI.Heisenberg.configPerm_swap_symm line 123
  20. theorem OAI.Heisenberg.star_matrixUnit line 129
  21. theorem OAI.Heisenberg.star_localUnit line 152
  22. theorem OAI.Heisenberg.star_spinZ line 157
  23. theorem OAI.Heisenberg.star_spinX line 161
  24. theorem OAI.Heisenberg.star_spinY line 165
  25. theorem OAI.Heisenberg.spinZ_mul_localUnit line 172
  26. theorem OAI.Heisenberg.localUnit_mul_spinZ line 179
  27. lemma OAI.Heisenberg.magneticLevel_succ line 186
  28. theorem OAI.Heisenberg.spinZ_spinPlus line 191
  29. theorem OAI.Heisenberg.spinZ_spinMinus line 204
  30. def OAI.Heisenberg.localAlgebra line 213
  31. lemma OAI.Heisenberg.localUnit_mem_localAlgebra line 216
  32. lemma OAI.Heisenberg.spinZ_mem_localAlgebra line 220
  33. lemma OAI.Heisenberg.spinPlus_mem_localAlgebra line 226
  34. lemma OAI.Heisenberg.spinMinus_mem_localAlgebra line 232
  35. lemma OAI.Heisenberg.spinX_mem_localAlgebra line 236
  36. lemma OAI.Heisenberg.spinY_mem_localAlgebra line 241
  37. theorem OAI.Heisenberg.localAlgebras_commute line 246
  38. lemma OAI.Heisenberg.singleton_local_commute line 272
  39. lemma OAI.Heisenberg.nearestNeighbor_ne line 277
  40. theorem OAI.Heisenberg.star_hamiltonian line 282
  41. instance OAI.Heisenberg.quasiLocalComplete line 299
  42. instance OAI.Heisenberg.quasiLocalRationalAlgebra line 302
  43. lemma OAI.Heisenberg.imaginaryTime_skew line 305
  44. lemma OAI.Heisenberg.hamiltonian_selfAdjoint line 309
  45. lemma OAI.Heisenberg.timeHamiltonian_skew line 312
  46. lemma OAI.Heisenberg.finiteUnitary line 316
  47. lemma OAI.Heisenberg.finiteInverseUnitary line 320
  48. theorem OAI.Heisenberg.norm_finiteDynamics line 324
  49. lemma OAI.Heisenberg.finiteDynamics_add line 329
  50. lemma OAI.Heisenberg.finiteDynamics_smul line 333
  51. lemma OAI.Heisenberg.finiteDynamics_sub line 337
  52. theorem OAI.Heisenberg.finiteDynamics_isometry line 341
  53. theorem OAI.Heisenberg.finiteDynamics_zero line 347
  54. lemma OAI.Heisenberg.exp_time_star line 351
  55. theorem OAI.Heisenberg.finiteDynamics_star line 357
  56. lemma OAI.Heisenberg.exp_time_inverse_left line 363
  57. lemma OAI.Heisenberg.exp_time_inverse_right line 369
  58. theorem OAI.Heisenberg.finiteDynamics_one line 375
  59. theorem OAI.Heisenberg.finiteDynamics_mul line 379
  60. lemma OAI.Heisenberg.exp_time_add line 390
  61. lemma OAI.Heisenberg.exp_time_neg line 397
  62. theorem OAI.Heisenberg.finiteDynamics_group line 402
  63. lemma OAI.Heisenberg.translation_localUnit line 408
  64. lemma OAI.Heisenberg.norm_translation line 413
  65. lemma OAI.Heisenberg.translation_spinZ line 418
  66. lemma OAI.Heisenberg.translation_spinPlus line 421
  67. lemma OAI.Heisenberg.translation_spinMinus line 424
  68. lemma OAI.Heisenberg.translation_spinX line 427
  69. lemma OAI.Heisenberg.translation_spinY line 429
  70. def OAI.Heisenberg.bond line 432
  71. def OAI.Heisenberg.bondBound line 435
  72. lemma OAI.Heisenberg.bondBound_nonneg line 438
  73. lemma OAI.Heisenberg.norm_bond_le line 440
  74. lemma OAI.Heisenberg.bond_mem_local line 455
  75. lemma OAI.Heisenberg.localAlgebra_mono line 466