OAI/Analysis/MatrixSigning/Complexity/PolynomialSearch.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.CurrentKS.Realization.poly_searchView line 13
2. instance OAI.CurrentKS.Realization.poly_searchPencil line 14
3. instance OAI.CurrentKS.Realization.poly_searchParameters line 15
4. instance OAI.CurrentKS.Realization.poly_searchY line 16
5. instance OAI.CurrentKS.Realization.poly_searchDim line 17
6. instance OAI.CurrentKS.Realization.poly_searchStep line 18
7. instance OAI.CurrentKS.Realization.poly_searchMesh line 19
8. instance OAI.CurrentKS.Realization.poly_searchInit line 20
9. lemma OAI.CurrentKS.Realization.runsPoly_searchFuel line 23
10. lemma OAI.CurrentKS.Realization.runsPoly_search line 39
11. def OAI.CurrentKS.Realization.searchResource line 48
12. lemma OAI.CurrentKS.Realization.search_cost_bound line 49