OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPropagationSampler.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Literal local propagation tables after adding the single reference bit. The arity is fixed in each program; no ambient spin configurations are scanned.

  1. abbrev OAI.ContinuumCoulomb.QuantumPropagationSampler.Input line 14
  2. abbrev OAI.ContinuumCoulomb.QuantumPropagationSampler.inputCode line 15
  3. def OAI.ContinuumCoulomb.QuantumPropagationSampler.coefficient line 17
  4. def OAI.ContinuumCoulomb.QuantumPropagationSampler.table line 19
  5. opaque OAI.ContinuumCoulomb.QuantumPropagationSampler.coefficientProgram line 24
  6. opaque OAI.ContinuumCoulomb.QuantumPropagationSampler.oneReferenceProgram line 38
  7. opaque OAI.ContinuumCoulomb.QuantumPropagationSampler.entryProgram line 48
  8. def OAI.ContinuumCoulomb.QuantumPropagationSampler.tableProgram line 57
  9. def OAI.ContinuumCoulomb.QuantumPropagationSampler.tableList line 62
  10. def OAI.ContinuumCoulomb.QuantumPropagationSampler.tableListProgram line 66
  11. theorem OAI.ContinuumCoulomb.QuantumPropagationSampler.matrixData_cast line 73
  12. def OAI.ContinuumCoulomb.QuantumPropagationSampler.basisEquiv line 79
  13. theorem OAI.ContinuumCoulomb.QuantumPropagationSampler.basisEquiv_zero line 86
  14. theorem OAI.ContinuumCoulomb.QuantumPropagationSampler.basisEquiv_succ line 93
  15. theorem OAI.ContinuumCoulomb.QuantumPropagationSampler.table_actual line 101
  16. theorem OAI.ContinuumCoulomb.QuantumPropagationSampler.tableList_actual line 112