OAI/MathematicalPhysics/Heisenberg/ExponentialEvolution.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SpinEvolution.leftRegular line 14
  2. lemma OAI.SpinEvolution.leftRegular_apply line 22
  3. lemma OAI.SpinEvolution.leftRegular_continuous line 24
  4. def OAI.SpinEvolution.rightRegular line 27
  5. lemma OAI.SpinEvolution.rightRegular_apply line 35
  6. lemma OAI.SpinEvolution.rightRegular_continuous line 37
  7. lemma OAI.SpinEvolution.left_right_commute line 40
  8. lemma OAI.SpinEvolution.exp_left line 47
  9. lemma OAI.SpinEvolution.exp_right line 52
  10. theorem OAI.SpinEvolution.exp_left_add_right line 60
  11. def OAI.SpinEvolution.generator line 67
  12. lemma OAI.SpinEvolution.generator_apply line 71
  13. lemma OAI.SpinEvolution.time_generator line 75
  14. theorem OAI.SpinEvolution.exp_generator line 81
  15. lemma OAI.SpinEvolution.exp_operator_apply line 86
  16. theorem OAI.SpinEvolution.dynamics_series line 91
  17. structure OAI.SpinEvolution.LocalDecomposition line 110
  18. theorem OAI.SpinEvolution.LocalDecomposition.power_bound line 116
  19. lemma OAI.SpinEvolution.summable_ascFactorial line 139
  20. def OAI.Heisenberg.neighbors line 165
  21. lemma OAI.Heisenberg.nearestNeighbor_symm line 169
  22. lemma OAI.Heisenberg.nearestNeighbor_coordinate line 174
  23. lemma OAI.Heisenberg.mem_neighbors_of_nearestNeighbor line 204
  24. lemma OAI.Heisenberg.card_neighbors_le line 223
  25. def OAI.Heisenberg.incidentEdges line 231
  26. lemma OAI.Heisenberg.mem_incidentEdges line 235
  27. lemma OAI.Heisenberg.card_incidentEdges_le line 243
  28. def OAI.Heisenberg.neighborhood line 256
  29. lemma OAI.Heisenberg.subset_neighborhood line 259
  30. lemma OAI.Heisenberg.nearestNeighbor_mem_neighborhood line 262