OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumEndpoint.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The verifier acceptance probability is the exact endpoint projection energy of its normalized zero-ancilla evolution.

  1. def OAI.ContinuumCoulomb.qmaInputVector line 12
  2. def OAI.ContinuumCoulomb.qmaOutputVector line 17
  3. def OAI.ContinuumCoulomb.qmaRejectVector line 22
  4. theorem OAI.ContinuumCoulomb.qmaInputVector_norm line 27
  5. theorem OAI.ContinuumCoulomb.qmaOutputVector_norm line 35
  6. theorem OAI.ContinuumCoulomb.qmaAcceptance_projection line 40
  7. theorem OAI.ContinuumCoulomb.qmaRejectVector_square line 51
  8. theorem OAI.ContinuumCoulomb.qmaRejectVector_of_accept line 60
  9. theorem OAI.ContinuumCoulomb.qmaRejectVector_of_sound line 66
  10. theorem OAI.ContinuumCoulomb.qmaApplyMatrix_smul line 72
  11. theorem OAI.ContinuumCoulomb.qmaInputVector_smul line 80
  12. theorem OAI.ContinuumCoulomb.qmaRejectVector_smul line 89