OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumHistoryDescriptors.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Literal numeric descriptors for the actual history terms, in the exact finite-sum order used before time grouping.

  1. abbrev OAI.ContinuumCoulomb.QuantumHistoryDescriptors.Descriptor line 13
  2. def OAI.ContinuumCoulomb.QuantumHistoryDescriptors.descriptorCode line 14
  3. def OAI.ContinuumCoulomb.QuantumHistoryDescriptors.encode line 16
  4. def OAI.ContinuumCoulomb.QuantumHistoryDescriptors.atIndex line 23
  5. theorem OAI.ContinuumCoulomb.QuantumHistoryDescriptors.atIndex_actual line 30
  6. def OAI.ContinuumCoulomb.QuantumHistoryDescriptors.source line 67
  7. theorem OAI.ContinuumCoulomb.QuantumHistoryDescriptors.source_actual line 70
  8. theorem OAI.ContinuumCoulomb.QuantumHistoryDescriptors.source_length line 82