OAI/Computability/QuantumFactoring/RetentionExpressionResources.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.lambdaE_poly line 13
2. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.coefficientE_poly line 18
3. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.remainderE_poly line 27
4. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.discrepancyE_poly line 31
5. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.thirdRetentionE_poly line 39
6. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.firstE_poly line 45
7. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.secondE_poly line 50
8. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.lastE_poly line 55
9. lemma OAI.ExactQuantumFactoring.thresholdExpr_poly line 63