OAI/MathematicalPhysics/Heisenberg/Model.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Heisenberg.L2 line 13

    Also declared: ComparatorChallenges/Heisenberg.lean:14 (same declaration text).

  2. def OAI.Heisenberg.l2Reindex line 15

    Also declared: ComparatorChallenges/Heisenberg.lean:16 (same declaration text).

  3. theorem OAI.Heisenberg.l2Reindex_apply line 31
  4. def OAI.Heisenberg.l2Projection line 34

    Also declared: ComparatorChallenges/Heisenberg.lean:32 (same declaration text).

  5. theorem OAI.Heisenberg.l2Projection_apply line 51
  6. abbrev OAI.Heisenberg.Site line 54

    Also declared: ComparatorChallenges/Heisenberg.lean:49 (same declaration text).

  7. abbrev OAI.Heisenberg.Level line 55

    Also declared: ComparatorChallenges/Heisenberg.lean:50 (same declaration text).

  8. abbrev OAI.Heisenberg.Configuration line 56

    Also declared: ComparatorChallenges/Heisenberg.lean:51 (same declaration text).

  9. abbrev OAI.Heisenberg.SpinHilbert line 57

    Also declared: ComparatorChallenges/Heisenberg.lean:52 (same declaration text).

  10. abbrev OAI.Heisenberg.SpinOperator line 58

    Also declared: ComparatorChallenges/Heisenberg.lean:53 (same declaration text).

  11. def OAI.Heisenberg.configPerm line 60

    Also declared: ComparatorChallenges/Heisenberg.lean:55 (same declaration text).

  12. def OAI.Heisenberg.matrixUnit line 73

    Also declared: ComparatorChallenges/Heisenberg.lean:68 (same declaration text).

  13. theorem OAI.Heisenberg.matrixUnit_apply line 77
  14. theorem OAI.Heisenberg.l2Reindex_symm_apply line 86
  15. def OAI.Heisenberg.operatorRelabel line 89

    Also declared: ComparatorChallenges/Heisenberg.lean:72 (same declaration text).

  16. theorem OAI.Heisenberg.relabel_matrixUnit line 93
  17. def OAI.Heisenberg.quasiLocalAlgebra line 115

    Also declared: ComparatorChallenges/Heisenberg.lean:76 (same declaration text).

  18. abbrev OAI.Heisenberg.QuasiLocal line 118

    Also declared: ComparatorChallenges/Heisenberg.lean:79 (same declaration text).

  19. def OAI.Heisenberg.localUnit line 120

    Also declared: ComparatorChallenges/Heisenberg.lean:81 (same declaration text).

  20. theorem OAI.Heisenberg.relabel_mem line 124
  21. def OAI.Heisenberg.translation line 140

    Also declared: ComparatorChallenges/Heisenberg.lean:85 (same declaration text).

  22. def OAI.Heisenberg.magneticLevel line 195

    Also declared: ComparatorChallenges/Heisenberg.lean:140 (same declaration text).

  23. def OAI.Heisenberg.spinZ line 197

    Also declared: ComparatorChallenges/Heisenberg.lean:142 (same declaration text).

  24. def OAI.Heisenberg.spinPlus line 200

    Also declared: ComparatorChallenges/Heisenberg.lean:145 (same declaration text).

  25. def OAI.Heisenberg.spinMinus line 206

    Also declared: ComparatorChallenges/Heisenberg.lean:151 (same declaration text).

  26. def OAI.Heisenberg.spinX line 208

    Also declared: ComparatorChallenges/Heisenberg.lean:153 (same declaration text).

  27. def OAI.Heisenberg.spinY line 211

    Also declared: ComparatorChallenges/Heisenberg.lean:156 (same declaration text).

  28. def OAI.Heisenberg.NearestNeighbor line 214

    Also declared: ComparatorChallenges/Heisenberg.lean:159 (same declaration text).

  29. def OAI.Heisenberg.volumeEdges line 217

    Also declared: ComparatorChallenges/Heisenberg.lean:162 (same declaration text).

  30. def OAI.Heisenberg.hamiltonian line 220

    Also declared: ComparatorChallenges/Heisenberg.lean:165 (same declaration text).

  31. def OAI.Heisenberg.box line 225

    Also declared: ComparatorChallenges/Heisenberg.lean:170 (same declaration text).

  32. def OAI.Heisenberg.finiteDynamics line 228

    Also declared: ComparatorChallenges/Heisenberg.lean:173 (same declaration text).

  33. def OAI.Heisenberg.dynamics line 233

    Also declared: ComparatorChallenges/Heisenberg.lean:178 (same declaration text).

  34. def OAI.Heisenberg.DynamicsConverges line 236

    Also declared: ComparatorChallenges/Heisenberg.lean:181 (same declaration text).

  35. structure OAI.Heisenberg.State line 241

    Also declared: ComparatorChallenges/Heisenberg.lean:186 (same declaration text).

  36. def OAI.Heisenberg.TranslationInvariant line 247

    Also declared: ComparatorChallenges/Heisenberg.lean:192 (same declaration text).

  37. def OAI.Heisenberg.IsKMS line 250

    Distinct definitions of this name: ComparatorChallenges/Heisenberg.lean:195 (same statement text; different proof or body). Qualify references as OAI.Heisenberg.IsKMS@path.