OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumOrderedDescriptorProgram.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

A literal polynomial program for the exact time-grouped descriptor list.

  1. abbrev OAI.ContinuumCoulomb.QuantumHistoryDescriptors.TimeInput line 12
  2. def OAI.ContinuumCoulomb.QuantumHistoryDescriptors.timeCode line 13
  3. opaque OAI.ContinuumCoulomb.QuantumHistoryDescriptors.timeValueProgram line 15
  4. abbrev OAI.ContinuumCoulomb.QuantumHistoryDescriptors.BucketInput line 42
  5. def OAI.ContinuumCoulomb.QuantumHistoryDescriptors.bucketCode line 43
  6. abbrev OAI.ContinuumCoulomb.QuantumHistoryDescriptors.ChunkInput line 44
  7. def OAI.ContinuumCoulomb.QuantumHistoryDescriptors.chunkCode line 45
  8. def OAI.ContinuumCoulomb.QuantumHistoryDescriptors.chunk line 47
  9. opaque OAI.ContinuumCoulomb.QuantumHistoryDescriptors.chunkProgram line 50
  10. theorem OAI.ContinuumCoulomb.QuantumHistoryDescriptors.chunks_eq line 60
  11. opaque OAI.ContinuumCoulomb.QuantumHistoryDescriptors.bucketProgram line 71
  12. opaque OAI.ContinuumCoulomb.QuantumHistoryDescriptors.orderedEntryProgram line 79
  13. opaque OAI.ContinuumCoulomb.QuantumHistoryDescriptors.orderedProgram line 85
  14. def OAI.ContinuumCoulomb.QuantumHistoryDescriptors.orderedCertificate line 92