OAI/Computability/QuantumFactoring/RationalExpressionResources.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ExactQuantumFactoring.PolyBound.twoPowSize line 13
  2. lemma OAI.ExactQuantumFactoring.NatExprPoly.ite line 20
  3. lemma OAI.ExactQuantumFactoring.NatExprPoly.constPoly line 26
  4. def OAI.ExactQuantumFactoring.IntExprPoly line 31

    Source documentation

    All balanced integer components have polynomial literal circuit syntax.

    def IntExprPoly {v : ℕ → Type*} (a : ∀ n, IntExpr (v n)) : Prop :=
…

    Mentions: OAI.ExactQuantumFactoring.IntExpr

  5. lemma OAI.ExactQuantumFactoring.IntExprPoly.ofNat line 35
  6. lemma OAI.ExactQuantumFactoring.IntExprPoly.ofInt line 38
  7. lemma OAI.ExactQuantumFactoring.IntExprPoly.negation line 43
  8. lemma OAI.ExactQuantumFactoring.IntExprPoly.add line 44
  9. lemma OAI.ExactQuantumFactoring.IntExprPoly.sub line 46
  10. lemma OAI.ExactQuantumFactoring.IntExprPoly.mul line 48
  11. lemma OAI.ExactQuantumFactoring.IntExprPoly.scale line 50
  12. lemma OAI.ExactQuantumFactoring.IntExprPoly.toNat line 52
  13. lemma OAI.ExactQuantumFactoring.IntExprPoly.natAbs line 53
  14. lemma OAI.ExactQuantumFactoring.IntExprPoly.iteLe line 55
  15. lemma OAI.ExactQuantumFactoring.IntExprPoly.ifLe line 59
  16. lemma OAI.ExactQuantumFactoring.IntExprPoly.ite line 63
  17. lemma OAI.ExactQuantumFactoring.IntExprPoly.signedPower line 68
  18. lemma OAI.ExactQuantumFactoring.IntExprPoly.ceilRatioNat line 72
  19. lemma OAI.ExactQuantumFactoring.IntExprPoly.floorRatio line 75
  20. def OAI.ExactQuantumFactoring.RatExprPoly line 81

    Source documentation

    Polynomial literal numerator and denominator syntax; no bound on dynamic values is assumed.

    def RatExprPoly {v : ℕ → Type*} (a : ∀ n, RatExpr (v n)) : Prop :=
…

    Mentions: OAI.ExactQuantumFactoring.RatExpr

  21. lemma OAI.ExactQuantumFactoring.RatExprPoly.ofNat line 85
  22. lemma OAI.ExactQuantumFactoring.RatExprPoly.ofInt line 88
  23. lemma OAI.ExactQuantumFactoring.RatExprPoly.const line 91
  24. lemma OAI.ExactQuantumFactoring.RatExprPoly.constant line 95
  25. lemma OAI.ExactQuantumFactoring.RatExprPoly.normalize line 97
  26. lemma OAI.ExactQuantumFactoring.RatExprPoly.add line 102
  27. lemma OAI.ExactQuantumFactoring.RatExprPoly.negation line 105
  28. lemma OAI.ExactQuantumFactoring.RatExprPoly.sub line 106
  29. lemma OAI.ExactQuantumFactoring.RatExprPoly.mul line 108
  30. lemma OAI.ExactQuantumFactoring.RatExprPoly.inverse line 110
  31. lemma OAI.ExactQuantumFactoring.RatExprPoly.div line 112
  32. lemma OAI.ExactQuantumFactoring.RatExprPoly.pow line 114
  33. lemma OAI.ExactQuantumFactoring.RatExprPoly.signedPower line 118
  34. lemma OAI.ExactQuantumFactoring.RatExprPoly.repeatedSuccess line 120
  35. lemma OAI.ExactQuantumFactoring.RatExprPoly.ifNatLe line 123
  36. lemma OAI.ExactQuantumFactoring.RatExprPoly.ifIntLe line 127
  37. lemma OAI.ExactQuantumFactoring.RatExprPoly.ifLe line 131
  38. lemma OAI.ExactQuantumFactoring.RatExprPoly.ifLt line 134
  39. lemma OAI.ExactQuantumFactoring.RatExprPoly.ifEq line 136
  40. lemma OAI.ExactQuantumFactoring.RatExprPoly.max line 138
  41. lemma OAI.ExactQuantumFactoring.RatExprPoly.min line 140
  42. lemma OAI.ExactQuantumFactoring.RatExprPoly.ceilNat line 142
  43. lemma OAI.ExactQuantumFactoring.RatExprPoly.floor line 143
  44. lemma OAI.ExactQuantumFactoring.RatExprPoly.ceil line 144