OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumListSchedule.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Validity, fixed-round termination and full-space energy bounds for the literal list-work routing compiler.

  1. theorem OAI.ContinuumCoulomb.QuantumListSchedule.partition_zero line 12
  2. theorem OAI.ContinuumCoulomb.QuantumListSchedule.partition_positive line 17
  3. theorem OAI.ContinuumCoulomb.QuantumListSchedule.erase_append line 23
  4. theorem OAI.ContinuumCoulomb.QuantumListSchedule.erase_block line 25
  5. theorem OAI.ContinuumCoulomb.QuantumListSchedule.erase_head line 30
  6. theorem OAI.ContinuumCoulomb.QuantumListSchedule.indexed_erase line 35
  7. theorem OAI.ContinuumCoulomb.QuantumListSchedule.erase_family line 41
  8. theorem OAI.ContinuumCoulomb.QuantumListSchedule.erase_value line 52
  9. theorem OAI.ContinuumCoulomb.QuantumListSchedule.partition_matrix line 57
  10. def OAI.ContinuumCoulomb.QuantumListSchedule.Valid line 70
  11. theorem OAI.ContinuumCoulomb.QuantumListSchedule.partition_valid line 73
  12. theorem OAI.ContinuumCoulomb.QuantumListSchedule.value_valid line 82
  13. def OAI.ContinuumCoulomb.QuantumListSchedule.energy line 92
  14. theorem OAI.ContinuumCoulomb.QuantumListSchedule.value_energy_error line 95
  15. theorem OAI.ContinuumCoulomb.QuantumListSchedule.indexed_mem line 109
  16. theorem OAI.ContinuumCoulomb.QuantumListSchedule.value_work_le line 118
  17. theorem OAI.ContinuumCoulomb.QuantumListSchedule.iterate_valid line 133
  18. theorem OAI.ContinuumCoulomb.QuantumListSchedule.iterate_work_le line 138
  19. theorem OAI.ContinuumCoulomb.QuantumListSchedule.iterate_complete line 145
  20. theorem OAI.ContinuumCoulomb.QuantumListSchedule.iterate_energy_error line 151
  21. theorem OAI.ContinuumCoulomb.QuantumListSchedule.partition_lengths line 163
  22. theorem OAI.ContinuumCoulomb.QuantumListSchedule.family_length line 170
  23. theorem OAI.ContinuumCoulomb.QuantumListSchedule.value_size line 180
  24. theorem OAI.ContinuumCoulomb.QuantumListSchedule.iterate_size line 187