OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumSpatialLattice.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The specified nearest-neighbor output of a degree-three spatial model. The graph, positions, source thresholds and estimates refer to one construction.

  1. def OAI.ContinuumCoulomb.QMASpatialExchangeModel.latticeGraph line 15
  2. def OAI.ContinuumCoulomb.QMASpatialExchangeModel.latticePosition line 19
  3. theorem OAI.ContinuumCoulomb.QMASpatialExchangeModel.lattice_vertices_ge line 23
  4. theorem OAI.ContinuumCoulomb.QMASpatialExchangeModel.lattice_position_injective line 27
  5. theorem OAI.ContinuumCoulomb.QMASpatialExchangeModel.lattice_adjacent line 32
  6. theorem OAI.ContinuumCoulomb.QMASpatialExchangeModel.lattice_bounded line 39
  7. theorem OAI.ContinuumCoulomb.QMASpatialExchangeModel.lattice_energy_error line 47
  8. theorem OAI.ContinuumCoulomb.QMASpatialExchangeModel.lattice_energy_error_nat line 53
  9. def OAI.ContinuumCoulomb.QMASpatialExchangeModel.latticeSource line 59
  10. theorem OAI.ContinuumCoulomb.QMASpatialExchangeModel.latticeSource_energy line 64
  11. theorem OAI.ContinuumCoulomb.QMASpatialExchangeModel.latticeSource_binary_promise line 70