OAI/MathematicalPhysics/Heisenberg/LocalDynamics.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Heisenberg.finiteGenerator line 11
  2. def OAI.Heisenberg.commutatorTerm line 14
  3. lemma OAI.Heisenberg.norm_commutatorTerm_le line 17
  4. lemma OAI.Heisenberg.finiteGenerator_eq_sum line 30
  5. lemma OAI.Heisenberg.commutatorTerm_mem line 36
  6. lemma OAI.Heisenberg.commutatorTerm_eq_zero line 46
  7. def OAI.Heisenberg.activeEdges line 57
  8. lemma OAI.Heisenberg.activeEdges_subset_incident line 60
  9. lemma OAI.Heisenberg.finiteGenerator_eq_activeSum line 66
  10. lemma OAI.Heisenberg.card_union_edge_le line 77
  11. def OAI.Heisenberg.SupportedOnAtMost line 91
  12. lemma OAI.Heisenberg.finiteGenerator_localDecomposition line 94
  13. lemma OAI.Heisenberg.activeEdges_stable line 129
  14. lemma OAI.Heisenberg.finiteGenerator_stable line 139
  15. lemma OAI.Heisenberg.finiteGenerator_local line 146
  16. theorem OAI.Heisenberg.eventually_mem_box line 162
  17. lemma OAI.Heisenberg.eventually_subset_box line 174
  18. theorem OAI.Heisenberg.local_coefficients_stabilize line 182
  19. def OAI.Heisenberg.localCore line 203
  20. theorem OAI.Heisenberg.localCore_dense line 206
  21. lemma OAI.Heisenberg.localCore_finite_support line 223
  22. lemma OAI.SpinEvolution.smul_operator_pow_apply line 254
  23. lemma OAI.SpinEvolution.exponential_operator_series line 262
  24. theorem OAI.SpinEvolution.local_exponential_converges line 274