OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumHistoryCells.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Natural cell lookups for the actual sparse history. The reference lookup uses the same time-grouped descriptors as the sampled Hamiltonian.

  1. def OAI.ContinuumCoulomb.QuantumHistoryCells.encodeCell line 16
  2. def OAI.ContinuumCoulomb.QuantumHistoryCells.gateCell line 19
  3. def OAI.ContinuumCoulomb.QuantumHistoryCells.referenceCell line 22
  4. def OAI.ContinuumCoulomb.QuantumHistoryCells.qubitCell line 25
  5. def OAI.ContinuumCoulomb.QuantumHistoryCells.termCell line 34
  6. def OAI.ContinuumCoulomb.QuantumHistoryCells.qubitCells line 38
  7. def OAI.ContinuumCoulomb.QuantumHistoryCells.referenceCells line 41
  8. def OAI.ContinuumCoulomb.QuantumHistoryCells.value line 44
  9. theorem OAI.ContinuumCoulomb.QuantumHistoryCells.patternCount_eq line 47
  10. theorem OAI.ContinuumCoulomb.QuantumHistoryCells.gateCell_actual line 50
  11. theorem OAI.ContinuumCoulomb.QuantumHistoryCells.referenceCell_actual line 58
  12. theorem OAI.ContinuumCoulomb.QuantumHistoryCells.qubitCell_actual line 66
  13. theorem OAI.ContinuumCoulomb.QuantumHistoryCells.termCell_actual line 95
  14. theorem OAI.ContinuumCoulomb.QuantumHistoryCells.qubitCells_actual line 115
  15. theorem OAI.ContinuumCoulomb.QuantumHistoryCells.referenceCells_actual line 129
  16. theorem OAI.ContinuumCoulomb.QuantumHistoryCells.sourceTerms_first line 142
  17. theorem OAI.ContinuumCoulomb.QuantumHistoryCells.anchors_source line 149
  18. theorem OAI.ContinuumCoulomb.QuantumHistoryCells.value_actual line 162