OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumAlgebraicScalar.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

Exact scalar arithmetic for the H,T,CNOT history compiler. A real scalar is a+b/sqrt(2); a complex scalar consists of two such pairs. The representation is rational data throughout, including multiplication.

  1. abbrev OAI.ContinuumCoulomb.QuantumAlgebraicScalar.RealScalar line 12
  2. abbrev OAI.ContinuumCoulomb.QuantumAlgebraicScalar.Scalar line 13
  3. def OAI.ContinuumCoulomb.QuantumAlgebraicScalar.realRat line 15
  4. def OAI.ContinuumCoulomb.QuantumAlgebraicScalar.realAdd line 16
  5. def OAI.ContinuumCoulomb.QuantumAlgebraicScalar.realNeg line 17
  6. def OAI.ContinuumCoulomb.QuantumAlgebraicScalar.realSub line 18
  7. def OAI.ContinuumCoulomb.QuantumAlgebraicScalar.realMul line 19
  8. def OAI.ContinuumCoulomb.QuantumAlgebraicScalar.rat line 21
  9. def OAI.ContinuumCoulomb.QuantumAlgebraicScalar.add line 22
  10. def OAI.ContinuumCoulomb.QuantumAlgebraicScalar.neg line 23
  11. def OAI.ContinuumCoulomb.QuantumAlgebraicScalar.sub line 24
  12. def OAI.ContinuumCoulomb.QuantumAlgebraicScalar.mul line 25
  13. def OAI.ContinuumCoulomb.QuantumAlgebraicScalar.conj line 28
  14. def OAI.ContinuumCoulomb.QuantumAlgebraicScalar.sqrtHalf line 29
  15. def OAI.ContinuumCoulomb.QuantumAlgebraicScalar.imaginary line 30
  16. def OAI.ContinuumCoulomb.QuantumAlgebraicScalar.realPart line 31
  17. def OAI.ContinuumCoulomb.QuantumAlgebraicScalar.imagPart line 32
  18. def OAI.ContinuumCoulomb.QuantumAlgebraicScalar.realValue line 34
  19. def OAI.ContinuumCoulomb.QuantumAlgebraicScalar.value line 36
  20. theorem OAI.ContinuumCoulomb.QuantumAlgebraicScalar.realValue_rat line 39
  21. theorem OAI.ContinuumCoulomb.QuantumAlgebraicScalar.realValue_add line 42
  22. theorem OAI.ContinuumCoulomb.QuantumAlgebraicScalar.realValue_neg line 47
  23. theorem OAI.ContinuumCoulomb.QuantumAlgebraicScalar.realValue_sub line 51
  24. theorem OAI.ContinuumCoulomb.QuantumAlgebraicScalar.realValue_mul line 55
  25. theorem OAI.ContinuumCoulomb.QuantumAlgebraicScalar.value_re line 61
  26. theorem OAI.ContinuumCoulomb.QuantumAlgebraicScalar.value_im line 64
  27. theorem OAI.ContinuumCoulomb.QuantumAlgebraicScalar.value_rat line 67
  28. theorem OAI.ContinuumCoulomb.QuantumAlgebraicScalar.value_add line 70
  29. theorem OAI.ContinuumCoulomb.QuantumAlgebraicScalar.value_neg line 73
  30. theorem OAI.ContinuumCoulomb.QuantumAlgebraicScalar.value_sub line 76
  31. theorem OAI.ContinuumCoulomb.QuantumAlgebraicScalar.value_mul line 79
  32. theorem OAI.ContinuumCoulomb.QuantumAlgebraicScalar.value_conj line 82
  33. theorem OAI.ContinuumCoulomb.QuantumAlgebraicScalar.value_sqrtHalf line 85
  34. theorem OAI.ContinuumCoulomb.QuantumAlgebraicScalar.value_imaginary line 88
  35. theorem OAI.ContinuumCoulomb.QuantumAlgebraicScalar.value_realPart line 91
  36. theorem OAI.ContinuumCoulomb.QuantumAlgebraicScalar.value_imagPart line 94
  37. def OAI.ContinuumCoulomb.QuantumAlgebraicScalar.sum line 97
  38. def OAI.ContinuumCoulomb.QuantumAlgebraicScalar.product line 101
  39. theorem OAI.ContinuumCoulomb.QuantumAlgebraicScalar.value_sum line 105
  40. theorem OAI.ContinuumCoulomb.QuantumAlgebraicScalar.value_product line 110
  41. def OAI.ContinuumCoulomb.QuantumAlgebraicScalar.sample line 115
  42. theorem OAI.ContinuumCoulomb.QuantumAlgebraicScalar.sample_error line 118