OAI/Analysis/MatrixSigning/Complexity/PolynomialRoots.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.CurrentKS.Realization.poly_wordTail line 14
2. instance OAI.CurrentKS.Realization.poly_ratFields line 15
3. instance OAI.CurrentKS.Realization.poly_ratNumBinary line 16
4. instance OAI.CurrentKS.Realization.poly_unframeNat line 17
5. instance OAI.CurrentKS.Realization.poly_ratDenBinary line 18
6. instance OAI.CurrentKS.Realization.poly_wordLength line 19
7. instance OAI.CurrentKS.Realization.poly_binarySize line 20
8. instance OAI.CurrentKS.Realization.poly_ratDenSize line 21
9. lemma OAI.CurrentKS.Realization.QParts.abs_le line 23
10. lemma OAI.CurrentKS.Realization.qparts_of_grid line 25
11. lemma OAI.CurrentKS.Realization.grid_mono line 36
12. lemma OAI.CurrentKS.Realization.grid_mid line 37
13. lemma OAI.CurrentKS.Realization.abs_mid line 43
14. lemma OAI.CurrentKS.Realization.root_iterate_invariant line 48
15. instance OAI.CurrentKS.Realization.poly_rootStep line 82
16. instance OAI.CurrentKS.Realization.size_rootStep line 84
17. instance OAI.CurrentKS.Realization.poly_rootRun line 107
18. instance OAI.CurrentKS.Realization.poly_upperSqrt line 108
19. instance OAI.CurrentKS.Realization.poly_approxPsi line 109