OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumAlgebraicHistory.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Actual ordered history cores have exact four-rational entries. The propagation Gram is formed on its at-most-five-site core; the construction does not sum over spectator configurations.

  1. def OAI.ContinuumCoulomb.QuantumAlgebraicHistory.denote line 15
  2. def OAI.ContinuumCoulomb.QuantumAlgebraicHistory.matMul line 18
  3. def OAI.ContinuumCoulomb.QuantumAlgebraicHistory.adjoint line 22
  4. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.denote_mul line 25
  5. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.denote_adjoint line 31
  6. def OAI.ContinuumCoulomb.QuantumAlgebraicHistory.hadamard line 36
  7. def OAI.ContinuumCoulomb.QuantumAlgebraicHistory.phaseT line 39
  8. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.value_hadamard line 42
  9. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.value_phaseT line 45
  10. def OAI.ContinuumCoulomb.QuantumAlgebraicHistory.identity line 48
  11. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.value_identity line 50
  12. def OAI.ContinuumCoulomb.QuantumAlgebraicHistory.gate line 54
  13. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.value_gate line 63
  14. def OAI.ContinuumCoulomb.QuantumAlgebraicHistory.delta line 86
  15. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.value_delta line 95
  16. def OAI.ContinuumCoulomb.QuantumAlgebraicHistory.deltaCore line 107
  17. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.denote_deltaCore line 112
  18. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.core_mul line 118
  19. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.core_adjoint line 126
  20. def OAI.ContinuumCoulomb.QuantumAlgebraicHistory.propagationCore line 133
  21. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.denote_propagationCore line 136
  22. def OAI.ContinuumCoulomb.QuantumAlgebraicHistory.lift line 143
  23. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.denote_lift line 149