OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumDiagonalTableProgram.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Fixed-arity scalar tables for the actual diagonal history terms. Only the local support bits are tabulated; the arity is at most six.

  1. abbrev OAI.ContinuumCoulomb.QuantumHistoryDiagonal.TableInput line 16
  2. def OAI.ContinuumCoulomb.QuantumHistoryDiagonal.tableCode line 17
  3. def OAI.ContinuumCoulomb.QuantumHistoryDiagonal.tableData line 20
  4. def OAI.ContinuumCoulomb.QuantumHistoryDiagonal.table line 23
  5. def OAI.ContinuumCoulomb.QuantumHistoryDiagonal.tableList line 26
  6. opaque OAI.ContinuumCoulomb.QuantumHistoryDiagonal.tableEntryInputProgram line 28
  7. def OAI.ContinuumCoulomb.QuantumHistoryDiagonal.tableEntryProgram line 38
  8. def OAI.ContinuumCoulomb.QuantumHistoryDiagonal.tableProgram line 46
  9. theorem OAI.ContinuumCoulomb.QuantumHistoryDiagonal.table_actual line 50
  10. theorem OAI.ContinuumCoulomb.QuantumHistoryDiagonal.tableList_actual line 60