OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumFixedMatrixProgram.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Literal arithmetic on a fixed local matrix table. These templates implement the adjoint-product and realification used in the actual history cores; their matrix dimensions are fixed before the program receives its rational registers.

  1. def OAI.ContinuumCoulomb.QuantumFixedMatrix.dataProgram line 16
  2. def OAI.ContinuumCoulomb.QuantumFixedMatrix.gramData line 27
  3. opaque OAI.ContinuumCoulomb.QuantumFixedMatrix.gramCellProgram line 30
  4. opaque OAI.ContinuumCoulomb.QuantumFixedMatrix.gramEntryProgram line 34
  5. def OAI.ContinuumCoulomb.QuantumFixedMatrix.gramProgram line 40
  6. theorem OAI.ContinuumCoulomb.QuantumFixedMatrix.gramData_matrixData line 44
  7. theorem OAI.ContinuumCoulomb.QuantumFixedMatrix.propagationData line 51
  8. def OAI.ContinuumCoulomb.QuantumFixedMatrix.rebitData line 55
  9. opaque OAI.ContinuumCoulomb.QuantumFixedMatrix.rebitEntryProgram line 58
  10. def OAI.ContinuumCoulomb.QuantumFixedMatrix.rebitProgram line 74
  11. theorem OAI.ContinuumCoulomb.QuantumFixedMatrix.rebitData_matrixData line 77