OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumInflatedListProgram.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The eightfold scaled route is an explicit list computation. Its loop bound is eight times the input route length.

  1. abbrev OAI.ContinuumCoulomb.QuantumInflatedListProgram.Input line 15
  2. def OAI.ContinuumCoulomb.QuantumInflatedListProgram.inputCode line 16
  3. def OAI.ContinuumCoulomb.QuantumInflatedListProgram.point line 17
  4. def OAI.ContinuumCoulomb.QuantumInflatedListProgram.value line 18
  5. opaque OAI.ContinuumCoulomb.QuantumInflatedListProgram.pointProgram line 21
  6. opaque OAI.ContinuumCoulomb.QuantumInflatedListProgram.lengthProgram line 33
  7. opaque OAI.ContinuumCoulomb.QuantumInflatedListProgram.indexedProgram line 40
  8. opaque OAI.ContinuumCoulomb.QuantumInflatedListProgram.tabProgram line 46
  9. opaque OAI.ContinuumCoulomb.QuantumInflatedListProgram.program line 50
  10. theorem OAI.ContinuumCoulomb.QuantumInflatedListProgram.length_value line 54
  11. theorem OAI.ContinuumCoulomb.QuantumInflatedListProgram.get_value line 57
  12. theorem OAI.ContinuumCoulomb.QuantumInflatedListProgram.lookup_range line 62
  13. theorem OAI.ContinuumCoulomb.QuantumInflatedListProgram.point_range line 66
  14. theorem OAI.ContinuumCoulomb.QuantumInflatedListProgram.value_range line 78