OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumRawCompiler.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Polynomial raw four-spin compiler with its full-space spectral guarantee.

  1. theorem OAI.ContinuumCoulomb.QuantumRawExchange.pack_weight line 14
  2. theorem OAI.ContinuumCoulomb.QuantumRawExchange.mass_packed line 17
  3. theorem OAI.ContinuumCoulomb.QuantumRawExchange.size_packed line 21
  4. theorem OAI.ContinuumCoulomb.QuantumRawExchange.budget_packed line 27
  5. theorem OAI.ContinuumCoulomb.QuantumRawExchange.scale_packed line 31
  6. theorem OAI.ContinuumCoulomb.QuantumRawExchange.bits_packed line 35
  7. def OAI.ContinuumCoulomb.QuantumRawExchange.rawBondMatrix line 42
  8. def OAI.ContinuumCoulomb.QuantumRawExchange.rawMatrix line 46
  9. theorem OAI.ContinuumCoulomb.QuantumRawExchange.rawBondMatrix_erase line 50
  10. theorem OAI.ContinuumCoulomb.QuantumRawExchange.fullMatrix_packed line 54
  11. theorem OAI.ContinuumCoulomb.QuantumRawExchange.compile_matrix line 62
  12. theorem OAI.ContinuumCoulomb.QuantumRawExchange.compile_accuracy line 68
  13. theorem OAI.ContinuumCoulomb.QuantumRawExchange.compile_valid line 76