OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumLatticeSerialization.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Literal serialization of rational lattice graphs into the published source format. The constant matrix offset is subtracted from both thresholds.

  1. abbrev OAI.ContinuumCoulomb.QuantumLatticeSerialization.Coordinate line 14
  2. abbrev OAI.ContinuumCoulomb.QuantumLatticeSerialization.Input line 15
  3. def OAI.ContinuumCoulomb.QuantumLatticeSerialization.coordinateCode line 16
  4. def OAI.ContinuumCoulomb.QuantumLatticeSerialization.thresholdCode line 17
  5. def OAI.ContinuumCoulomb.QuantumLatticeSerialization.inputCode line 18
  6. def OAI.ContinuumCoulomb.QuantumLatticeSerialization.edge line 21
  7. def OAI.ContinuumCoulomb.QuantumLatticeSerialization.value line 22
  8. def OAI.ContinuumCoulomb.QuantumLatticeSerialization.rationalProgram line 28
  9. def OAI.ContinuumCoulomb.QuantumLatticeSerialization.coordinateProgram line 33
  10. def OAI.ContinuumCoulomb.QuantumLatticeSerialization.edgeProgram line 38
  11. def OAI.ContinuumCoulomb.QuantumLatticeSerialization.coordinatesProgram line 47
  12. def OAI.ContinuumCoulomb.QuantumLatticeSerialization.bondsProgram line 52
  13. def OAI.ContinuumCoulomb.QuantumLatticeSerialization.thresholdsProgram line 58
  14. def OAI.ContinuumCoulomb.QuantumLatticeSerialization.program line 69
  15. def OAI.ContinuumCoulomb.QuantumLatticeSerialization.certificate line 75
  16. theorem OAI.ContinuumCoulomb.QuantumLatticeSerialization.lower_value line 78
  17. theorem OAI.ContinuumCoulomb.QuantumLatticeSerialization.upper_value line 80
  18. theorem OAI.ContinuumCoulomb.QuantumLatticeSerialization.edges_length line 82