OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumHistoryHeight.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Polynomial bounds for the actual rational-register history entries. The only matrix multiplication takes place on the five-site propagation core, with at most32 intermediate configurations.

  1. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.height_identity line 15
  2. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.height_hadamard line 19
  3. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.height_phaseT line 24
  4. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.height_single_product line 29
  5. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.height_gate line 44
  6. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.height_delta line 53
  7. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.propagation_configurations line 70
  8. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.height_propagationCore line 76
  9. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.height_lift line 96
  10. def OAI.ContinuumCoulomb.QuantumAlgebraicHistory.historyHeight line 105
  11. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.historyHeight_nonnegative line 108
  12. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.height_distributed line 112
  13. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.height_localY line 141
  14. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.height_rebit line 150
  15. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.height_pairY line 169
  16. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.height_referenceEdge line 179
  17. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.height_orderedTerm line 198
  18. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.height_orderedCore line 214
  19. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.orderedCoefficient_height line 220