OAI/Computability/QuantumFactoring/RetainedNetworkPolynomial.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.RetainedPolynomial.primeComponentBound_at line 17
2. lemma OAI.ExactQuantumFactoring.RetainedPolynomial.tableOrderBound_at line 26
3. lemma OAI.ExactQuantumFactoring.RetainedPolynomial.totientStepBound_at line 35
4. lemma OAI.ExactQuantumFactoring.RetainedPolynomial.tableTotientBound_at line 37
5. lemma OAI.ExactQuantumFactoring.RetainedPolynomial.oddPartBound_at line 41
6. lemma OAI.ExactQuantumFactoring.RetainedPolynomial.closedLevelBound_at line 45
7. lemma OAI.ExactQuantumFactoring.RetainedPolynomial.componentLevelBound_at line 49
8. lemma OAI.ExactQuantumFactoring.RetainedPolynomial.tableFavorableCountBound_at line 55
9. lemma OAI.ExactQuantumFactoring.RetainedPolynomial.tableCanonicalBound_at line 67
10. lemma OAI.ExactQuantumFactoring.RetainedPolynomial.resultBound_at line 79