OAI/Computability/QuantumFactoring/PolyBounds.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.PolyBound line 12

   Source documentation

   A worst-case bound for all input lengths, with nonnegative coefficients.

   def PolyBound (f : ℕ → ℕ) : Prop :=
   …

2. lemma OAI.ExactQuantumFactoring.PolyBound.const line 16
3. lemma OAI.ExactQuantumFactoring.PolyBound.id line 18
4. lemma OAI.ExactQuantumFactoring.PolyBound.add line 19
5. lemma OAI.ExactQuantumFactoring.PolyBound.mul line 24
6. lemma OAI.ExactQuantumFactoring.PolyBound.pow line 29
7. lemma OAI.ExactQuantumFactoring.PolyBound.of_le line 33
8. lemma OAI.ExactQuantumFactoring.PolyBound.max line 36
9. lemma OAI.ExactQuantumFactoring.PolyBound.sub line 39
10. lemma OAI.ExactQuantumFactoring.PolyBound.div line 41
11. lemma OAI.ExactQuantumFactoring.PolyBound.mod line 43
12. lemma OAI.ExactQuantumFactoring.PolyBound.ite line 45
13. lemma OAI.ExactQuantumFactoring.PolyBound.eval_mono line 50
14. lemma OAI.ExactQuantumFactoring.PolyBound.comp line 56
15. lemma OAI.ExactQuantumFactoring.PolyBound.natSize line 64