OAI/Analysis/MatrixSigning/Complexity/PolynomialRoundedStep.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.CurrentKS.Realization.poly_roundedUpdate line 14
2. instance OAI.CurrentKS.Realization.poly_stateView line 15
3. instance OAI.CurrentKS.Realization.poly_statePencil line 16
4. instance OAI.CurrentKS.Realization.poly_stateParameters line 17
5. instance OAI.CurrentKS.Realization.poly_stateY line 18
6. instance OAI.CurrentKS.Realization.poly_stateWitness line 19
7. instance OAI.CurrentKS.Realization.poly_stateNextVector line 20
8. instance OAI.CurrentKS.Realization.poly_pencilNext line 21
9. lemma OAI.CurrentKS.Realization.round_abs line 23
10. lemma OAI.CurrentKS.Realization.l1_coordinate line 39
11. lemma OAI.CurrentKS.Realization.pencil_next_abs line 47
12. lemma OAI.CurrentKS.Realization.pencil_next_grid line 61
13. lemma OAI.CurrentKS.Realization.pencil_iterate_parts line 69
14. instance OAI.CurrentKS.Realization.size_pencilNext line 98