OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPropagationTable.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Exact fixed-size propagation tables and their adjoint-product. The largest table has five qubits, independently of the circuit work register.

  1. abbrev OAI.ContinuumCoulomb.QuantumPropagationTable.Input line 16
  2. def OAI.ContinuumCoulomb.QuantumPropagationTable.inputCode line 17
  3. def OAI.ContinuumCoulomb.QuantumPropagationTable.data line 20
  4. def OAI.ContinuumCoulomb.QuantumPropagationTable.table line 23
  5. opaque OAI.ContinuumCoulomb.QuantumPropagationTable.entryInputProgram line 26
  6. opaque OAI.ContinuumCoulomb.QuantumPropagationTable.entryProgram line 38
  7. def OAI.ContinuumCoulomb.QuantumPropagationTable.tableProgram line 43
  8. def OAI.ContinuumCoulomb.QuantumPropagationTable.gramProgram line 48
  9. def OAI.ContinuumCoulomb.QuantumPropagationTable.supportBasisEquiv line 54
  10. theorem OAI.ContinuumCoulomb.QuantumPropagationTable.table_actual line 59
  11. theorem OAI.ContinuumCoulomb.QuantumPropagationTable.gram_actual line 69
  12. theorem OAI.ContinuumCoulomb.QuantumPropagationTable.gramData_actual line 78