OAI/Computability/QuantumFactoring/PolyAt.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.PolyAt line 14

    Source documentation

    Uniform polynomial bounds over arbitrary auxiliary parameters. Only the chosen length is charged, so this also records worst-case bounds over all finite loop indices and all networks satisfying a supplied count invariant.

    def PolyAt {α : Sort*} (length : α→ℕ) (f : α→ℕ) : Prop :=
…
  2. lemma OAI.ExactQuantumFactoring.PolyAt.const line 18
  3. lemma OAI.ExactQuantumFactoring.PolyAt.self line 20
  4. lemma OAI.ExactQuantumFactoring.PolyAt.add line 21
  5. lemma OAI.ExactQuantumFactoring.PolyAt.mul line 24
  6. lemma OAI.ExactQuantumFactoring.PolyAt.pow line 27
  7. lemma OAI.ExactQuantumFactoring.PolyAt.of_le line 30
  8. lemma OAI.ExactQuantumFactoring.PolyAt.sub line 33
  9. lemma OAI.ExactQuantumFactoring.PolyAt.div line 34
  10. lemma OAI.ExactQuantumFactoring.PolyAt.mod line 35
  11. lemma OAI.ExactQuantumFactoring.PolyAt.max line 36
  12. lemma OAI.ExactQuantumFactoring.PolyAt.ite line 38
  13. lemma OAI.ExactQuantumFactoring.PolyAt.pull line 41
  14. lemma OAI.ExactQuantumFactoring.PolyAt.ofPoly line 44
  15. lemma OAI.ExactQuantumFactoring.PolyAt.comp line 46
  16. lemma OAI.ExactQuantumFactoring.PolyAt.natSize line 52