OAI/Computability/QuantumFactoring/PolynomialFilterExpressions.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.NatExpr.pow line 14
  2. lemma OAI.ExactQuantumFactoring.NatExpr.eval_pow line 17
  3. def OAI.ExactQuantumFactoring.RatExpr.sumList line 26
  4. lemma OAI.ExactQuantumFactoring.RatExpr.eval_sumList line 29
  5. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.rampPoly line 40
  6. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.rampLin line 42
  7. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.rampPoly_correct line 44
  8. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.rampLin_correct line 47
  9. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.splineRePoly line 51
  10. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.splineImPoly line 54
  11. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.phaseRePoly line 57
  12. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.phaseImPoly line 59
  13. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.splineRePoly_correct line 62
  14. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.splineImPoly_correct line 65
  15. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.phaseRePoly_correct line 68
  16. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.phaseImPoly_correct line 71
  17. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.linearPoly line 75
  18. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.linearPoly_correct line 76
  19. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.integralZero line 80
  20. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.integralSlope line 82
  21. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.massZero line 84
  22. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.massSlope line 86
  23. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.massCoeff line 90
  24. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.massCoeff_correct line 92
  25. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.rounded line 100
  26. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.rounded_correct line 102
  27. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.roundingDen line 106
  28. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.roundingDen_correct line 107
  29. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.low line 111
  30. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.high line 113
  31. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.low_correct line 116
  32. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.high_correct line 119
  33. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.pieceSum line 123
  34. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.pieceSum_correct line 129
  35. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.quarterList line 136

    Source documentation

    Literal fixed 32-piece table; no noncomputable Finset enumeration is used by the circuit generator.

    def quarterList : List (ℤ×ℤ) :=
…
  36. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.quarterList_nodup line 138
  37. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.quarterList_finset line 139
  38. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.majorantSumE line 141
  39. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.majorantSumE_correct line 143