OAI/Analysis/MatrixSigning/Optimization/SearchStep.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CurrentKS.RationalSDP.searchStep line 14
2. def OAI.CurrentKS.RationalSDP.searchMesh line 15
3. def OAI.CurrentKS.RationalSDP.searchFuel line 17
4. def OAI.CurrentKS.RationalSDP.Pencil.search line 20
5. lemma OAI.CurrentKS.RationalSDP.searchStep_pos line 23
6. lemma OAI.CurrentKS.RationalSDP.searchMesh_pos line 27
7. lemma OAI.CurrentKS.RationalSDP.mesh_error_small line 32
8. lemma OAI.CurrentKS.RationalSDP.searchMesh_small line 46
9. lemma OAI.CurrentKS.RationalSDP.searchFuel_suffices line 64
10. theorem OAI.CurrentKS.RationalSDP.Pencil.search_accepts line 79
11. lemma OAI.CurrentKS.RationalSDP.roundVector_on_mesh line 89
12. lemma OAI.CurrentKS.RationalSDP.Pencil.next_on_mesh line 94
13. lemma OAI.CurrentKS.RationalSDP.Pencil.iterate_on_mesh line 102