OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumCoefficientEnvelopeProgram.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Literal unary programs for the logical and physical coefficient bounds. The only arguments are qubit count, term count, initial magnitude and precision.

  1. def OAI.ContinuumCoulomb.QuantumCoefficientEnvelopeProgram.add line 14
  2. def OAI.ContinuumCoulomb.QuantumCoefficientEnvelopeProgram.mul line 17
  3. def OAI.ContinuumCoulomb.QuantumCoefficientEnvelopeProgram.constant line 20
  4. def OAI.ContinuumCoulomb.QuantumCoefficientEnvelopeProgram.square line 22
  5. def OAI.ContinuumCoulomb.QuantumCoefficientEnvelopeProgram.cube line 25
  6. def OAI.ContinuumCoulomb.QuantumCoefficientEnvelopeProgram.fourth line 28
  7. opaque OAI.ContinuumCoulomb.QuantumCoefficientEnvelopeProgram.weightProgram line 32
  8. opaque OAI.ContinuumCoulomb.QuantumCoefficientEnvelopeProgram.logicalScaleProgram line 39
  9. opaque OAI.ContinuumCoulomb.QuantumCoefficientEnvelopeProgram.stepProgram line 47
  10. def OAI.ContinuumCoulomb.QuantumCoefficientEnvelopeProgram.logicalProgram line 53
  11. opaque OAI.ContinuumCoulomb.QuantumCoefficientEnvelopeProgram.rawBudgetProgram line 61
  12. opaque OAI.ContinuumCoulomb.QuantumCoefficientEnvelopeProgram.rawScaleProgram line 69
  13. opaque OAI.ContinuumCoulomb.QuantumCoefficientEnvelopeProgram.rawOutputProgram line 75
  14. abbrev OAI.ContinuumCoulomb.QuantumCoefficientEnvelopeProgram.Input line 85
  15. def OAI.ContinuumCoulomb.QuantumCoefficientEnvelopeProgram.inputCode line 86
  16. def OAI.ContinuumCoulomb.QuantumCoefficientEnvelopeProgram.value line 87
  17. opaque OAI.ContinuumCoulomb.QuantumCoefficientEnvelopeProgram.program line 91
  18. theorem OAI.ContinuumCoulomb.QuantumCoefficientEnvelopeProgram.polynomial_bound line 101