OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumListScheduleGraph.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

The actual edge-indexed schedule represented by a literal bond/work tape.

  1. def OAI.ContinuumCoulomb.QuantumListSchedule.graph line 13
  2. def OAI.ContinuumCoulomb.QuantumListSchedule.schedule line 24
  3. theorem OAI.ContinuumCoulomb.QuantumListSchedule.graph_packed line 28
  4. theorem OAI.ContinuumCoulomb.QuantumListSchedule.graph_energy line 33
  5. theorem OAI.ContinuumCoulomb.QuantumListSchedule.schedule_active line 38
  6. def OAI.ContinuumCoulomb.QuantumListSchedule.indices line 42
  7. theorem OAI.ContinuumCoulomb.QuantumListSchedule.indices_nodup line 45
  8. theorem OAI.ContinuumCoulomb.QuantumListSchedule.indices_map line 48
  9. theorem OAI.ContinuumCoulomb.QuantumListSchedule.mem_indices line 57
  10. theorem OAI.ContinuumCoulomb.QuantumListSchedule.indices_length line 61
  11. def OAI.ContinuumCoulomb.QuantumListSchedule.indexEquiv line 66
  12. theorem OAI.ContinuumCoulomb.QuantumListSchedule.indexEquiv_get line 72
  13. theorem OAI.ContinuumCoulomb.QuantumListSchedule.selected_true_iff line 80
  14. theorem OAI.ContinuumCoulomb.QuantumListSchedule.selected_false_iff line 86
  15. def OAI.ContinuumCoulomb.QuantumListSchedule.activeEquiv line 89
  16. def OAI.ContinuumCoulomb.QuantumListSchedule.retainedEquiv line 94
  17. def OAI.ContinuumCoulomb.QuantumListSchedule.activePermutation line 101