OAI/MathematicalPhysics/Heisenberg/SlotOnMesh.lean

GitHub source file

85 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Heisenberg.SpinSlots.Config line 9
  2. abbrev OAI.Heisenberg.SpinSlots.Level line 10
  3. def OAI.Heisenberg.SpinSlots.basis line 12
  4. lemma OAI.Heisenberg.SpinSlots.config_card_le line 15
  5. lemma OAI.Heisenberg.SpinSlots.multiplicity_pos line 18
  6. lemma OAI.Heisenberg.SpinSlots.sqrt_multiplicity_pos line 21
  7. lemma OAI.Heisenberg.SpinSlots.basis_nonneg line 24
  8. lemma OAI.Heisenberg.SpinSlots.card_layer line 28
  9. theorem OAI.Heisenberg.SpinSlots.basis_orthonormal line 36
  10. def OAI.Heisenberg.SpinSlots.raising line 63
  11. def OAI.Heisenberg.SpinSlots.diagonalZ line 66
  12. def OAI.Heisenberg.SpinSlots.physicalZ line 69
  13. def OAI.Heisenberg.SpinSlots.physicalPlus line 72
  14. lemma OAI.Heisenberg.SpinSlots.raising_mul_basis line 75
  15. lemma OAI.Heisenberg.SpinSlots.binomial_raising_coefficient line 83
  16. lemma OAI.Heisenberg.SpinSlots.raising_coefficient_source line 106
  17. lemma OAI.Heisenberg.SpinSlots.raising_basis_entry line 112
  18. theorem OAI.Heisenberg.SpinSlots.diagonal_intertwines line 127
  19. theorem OAI.Heisenberg.SpinSlots.raising_intertwines line 132
  20. def OAI.Heisenberg.SpinSlots.average line 159
  21. lemma OAI.Heisenberg.SpinSlots.map_mul line 163
  22. lemma OAI.Heisenberg.SpinSlots.average_map_left line 168
  23. lemma OAI.Heisenberg.SpinSlots.average_column_sum line 179
  24. lemma OAI.Heisenberg.SpinSlots.average_eq_zero line 185
  25. lemma OAI.Heisenberg.SpinSlots.average_eq_diagonal line 193
  26. lemma OAI.Heisenberg.SpinSlots.average_diagonal line 198
  27. theorem OAI.Heisenberg.SpinSlots.average_entry line 216
  28. lemma OAI.Heisenberg.SpinSlots.basis_projection_entry line 222
  29. theorem OAI.Heisenberg.SpinSlots.symmetrizer line 240
  30. lemma OAI.Heisenberg.SpinSlots.erase_relation line 244
  31. lemma OAI.Heisenberg.SpinSlots.lowering_entry line 252
  32. lemma OAI.Heisenberg.SpinSlots.lowering_mul_basis line 263
  33. lemma OAI.Heisenberg.SpinSlots.lowering_basis_entry line 272
  34. lemma OAI.Heisenberg.SpinSlots.binomial_lowering_coefficient line 286
  35. theorem OAI.Heisenberg.SpinSlots.lowering_intertwines line 308
  36. def OAI.Heisenberg.TensorMatrix.tensor line 349
  37. lemma OAI.Heisenberg.TensorMatrix.tensor_mul line 352
  38. lemma OAI.Heisenberg.TensorMatrix.tensor_one line 359
  39. lemma OAI.Heisenberg.TensorMatrix.tensor_transpose line 370
  40. lemma OAI.Heisenberg.TensorMatrix.tensor_trace line 373
  41. def OAI.Heisenberg.TensorMatrix.onsite line 378
  42. lemma OAI.Heisenberg.TensorMatrix.local_one line 382
  43. lemma OAI.Heisenberg.TensorMatrix.local_mul line 386
  44. lemma OAI.Heisenberg.TensorMatrix.local_entry line 394
  45. lemma OAI.Heisenberg.TensorMatrix.local_add line 405
  46. lemma OAI.Heisenberg.TensorMatrix.local_zero line 410
  47. lemma OAI.Heisenberg.TensorMatrix.local_smul line 415
  48. lemma OAI.Heisenberg.TensorMatrix.local_commute line 420
  49. lemma OAI.Heisenberg.TensorMatrix.local_intertwines line 433
  50. lemma OAI.Heisenberg.TensorMatrix.tensor_orthonormal line 445
  51. def OAI.Heisenberg.SlotTensor.configEquiv line 457
  52. lemma OAI.Heisenberg.SlotTensor.mem_configEquiv line 466
  53. def OAI.Heisenberg.SlotTensor.fiberPerm line 470
  54. lemma OAI.Heisenberg.SlotTensor.configEquiv_fiberPerm line 477
  55. def OAI.Heisenberg.SlotTensor.matrix line 484
  56. lemma OAI.Heisenberg.SlotTensor.matrix_fiberPerm line 489
  57. theorem OAI.Heisenberg.SlotTensor.symmetrizer line 508
  58. lemma OAI.Heisenberg.SlotTensor.basis_orthonormal line 520
  59. lemma OAI.Heisenberg.SlotTensor.raising_intertwines line 524
  60. lemma OAI.Heisenberg.SlotTensor.lowering_intertwines line 529
  61. lemma OAI.Heisenberg.SlotTensor.diagonal_intertwines line 534
  62. def OAI.Heisenberg.SlotHalf.change line 544
  63. def OAI.Heisenberg.SlotHalf.z line 547
  64. lemma OAI.Heisenberg.SlotHalf.change_entry line 550
  65. lemma OAI.Heisenberg.SlotHalf.change_mul line 554
  66. lemma OAI.Heisenberg.SlotHalf.swapped_same line 568
  67. lemma OAI.Heisenberg.SlotHalf.swapped_different line 578
  68. theorem OAI.Heisenberg.SlotHalf.swap_spin line 588
  69. lemma OAI.Heisenberg.TensorMatrix.local_entry_ite line 629
  70. lemma OAI.Heisenberg.SlotTensor.config_update_true line 652
  71. lemma OAI.Heisenberg.SlotTensor.reindex_change_true_entry line 663
  72. lemma OAI.Heisenberg.SlotTensor.erase_insert_condition line 675
  73. theorem OAI.Heisenberg.SlotTensor.slot_raising line 683
  74. lemma OAI.Heisenberg.SlotHalf.change_transpose line 705
  75. lemma OAI.Heisenberg.TensorMatrix.local_transpose line 721
  76. lemma OAI.Heisenberg.TensorMatrix.local_diagonal line 727
  77. theorem OAI.Heisenberg.SlotTensor.slot_lowering line 749
  78. theorem OAI.Heisenberg.SlotTensor.slot_z line 760
  79. def OAI.Heisenberg.SlotHalf.totalPlus line 786
  80. def OAI.Heisenberg.SlotHalf.totalMinus line 787
  81. def OAI.Heisenberg.SlotHalf.totalZ line 788
  82. theorem OAI.Heisenberg.SlotHalf.cross_site_swaps line 790
  83. def OAI.Heisenberg.SlotTensor.spinBond line 815
  84. def OAI.Heisenberg.SlotTensor.slotBond line 820
  85. theorem OAI.Heisenberg.SlotTensor.bond_intertwines line 825