OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumSpacedListProgram.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Enumerate the bounded Manhattan portion of each actual buffered route. The horizontal and vertical translations are literal binary arithmetic.

  1. def OAI.ContinuumCoulomb.QuantumSpacedListProgram.point line 13
  2. abbrev OAI.ContinuumCoulomb.QuantumSpacedListProgram.PointInput line 16
  3. def OAI.ContinuumCoulomb.QuantumSpacedListProgram.pointCode line 17
  4. def OAI.ContinuumCoulomb.QuantumSpacedListProgram.pointProgram line 19
  5. abbrev OAI.ContinuumCoulomb.QuantumSpacedListProgram.Input line 27
  6. def OAI.ContinuumCoulomb.QuantumSpacedListProgram.inputCode line 28
  7. def OAI.ContinuumCoulomb.QuantumSpacedListProgram.budget line 29
  8. def OAI.ContinuumCoulomb.QuantumSpacedListProgram.value line 30
  9. def OAI.ContinuumCoulomb.QuantumSpacedListProgram.program line 33
  10. theorem OAI.ContinuumCoulomb.QuantumSpacedListProgram.point_actual line 40
  11. theorem OAI.ContinuumCoulomb.QuantumSpacedListProgram.value_actual line 43