OAI/Computability/QuantumFactoring/ProgressionExpressions.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.NatExpr.min line 17
  2. def OAI.ExactQuantumFactoring.NatExpr.max line 18
  3. lemma OAI.ExactQuantumFactoring.NatExpr.eval_min line 19
  4. lemma OAI.ExactQuantumFactoring.NatExpr.eval_max line 21
  5. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.powerSum line 29
  6. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.powerSum_correct line 36
  7. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.fiveTerm line 40
  8. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.fiveTerm_correct line 42
  9. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.linear line 46
  10. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.linear_correct line 48
  11. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.ramp line 55
  12. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.ramp_correct line 59
  13. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.phaseRe line 63
  14. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.phaseRe_correct line 66
  15. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.phaseIm line 70
  16. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.phaseIm_correct line 73
  17. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.binE line 77
  18. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.binE_correct line 79
  19. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.error line 82
  20. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.error_correct line 83
  21. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.offset line 87
  22. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.offset_correct line 89
  23. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.slope line 93
  24. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.slope_correct line 94
  25. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.count line 98
  26. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.count_correct line 99
  27. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.probability line 104

    Source documentation

    A literal finite arithmetic template for P. Its size is independent of Q, B,d,j,t; there is no enumeration of the phase-register range.

    def probability (Q d j t : NatExpr v) : RatExpr v :=
…

    Mentions: OAI.ExactQuantumFactoring.NatExpr, OAI.ExactQuantumFactoring.RatExpr

  28. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.probability_correct line 107