OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumHistoryPrecisionProgram.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

The prescribed sampling precision is computed in unary. Composition with the checked local sampler yields the actual early raw exchange compiler.

  1. abbrev OAI.ContinuumCoulomb.QuantumHistoryPrecisionProgram.Input line 13
  2. abbrev OAI.ContinuumCoulomb.QuantumHistoryPrecisionProgram.inputCode line 14
  3. opaque OAI.ContinuumCoulomb.QuantumHistoryPrecisionProgram.coefficientBudgetProgram line 16
  4. opaque OAI.ContinuumCoulomb.QuantumHistoryPrecisionProgram.termBudgetProgram line 27
  5. opaque OAI.ContinuumCoulomb.QuantumHistoryPrecisionProgram.circuitProgram line 34
  6. opaque OAI.ContinuumCoulomb.QuantumHistoryPrecisionProgram.inverseErrorProgram line 36
  7. opaque OAI.ContinuumCoulomb.QuantumHistoryPrecisionProgram.termAllowanceProgram line 39
  8. opaque OAI.ContinuumCoulomb.QuantumHistoryPrecisionProgram.coefficientAllowanceProgram line 43
  9. opaque OAI.ContinuumCoulomb.QuantumHistoryPrecisionProgram.precisionFactorProgram line 47
  10. opaque OAI.ContinuumCoulomb.QuantumHistoryPrecisionProgram.precisionProgram line 51
  11. opaque OAI.ContinuumCoulomb.QuantumHistoryPrecisionProgram.sourceQubitsProgram line 56
  12. def OAI.ContinuumCoulomb.QuantumHistoryPrecisionProgram.prepare line 66
  13. opaque OAI.ContinuumCoulomb.QuantumHistoryPrecisionProgram.prepareProgram line 70
  14. def OAI.ContinuumCoulomb.QuantumHistoryPrecisionProgram.output line 74
  15. opaque OAI.ContinuumCoulomb.QuantumHistoryPrecisionProgram.outputProgram line 77
  16. def OAI.ContinuumCoulomb.QuantumHistoryPrecisionProgram.physicalQubits line 81
  17. theorem OAI.ContinuumCoulomb.QuantumHistoryPrecisionProgram.physicalQubits_eq line 83
  18. opaque OAI.ContinuumCoulomb.QuantumHistoryPrecisionProgram.outputCountProgram line 88
  19. opaque OAI.ContinuumCoulomb.QuantumHistoryPrecisionProgram.physicalQubitsProgram line 92
  20. theorem OAI.ContinuumCoulomb.QuantumHistoryPrecisionProgram.prepare_actual line 96
  21. theorem OAI.ContinuumCoulomb.QuantumHistoryPrecisionProgram.output_actual line 104
  22. theorem OAI.ContinuumCoulomb.QuantumHistoryPrecisionProgram.physicalQubits_actual line 108
  23. def OAI.ContinuumCoulomb.QuantumHistoryPrecisionProgram.certificate line 112