OAI/Analysis/MatrixSigning/Complexity/PolynomialMatrixFold.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CurrentKS.Realization.QParts line 14
2. lemma OAI.CurrentKS.Realization.QParts.mono line 15
3. lemma OAI.CurrentKS.Realization.qparts_zero line 17
4. lemma OAI.CurrentKS.Realization.qparts_length line 18
5. lemma OAI.CurrentKS.Realization.QParts.mul line 19
6. lemma OAI.CurrentKS.Realization.QParts.add line 21
7. lemma OAI.CurrentKS.Realization.QParts.length line 24
8. lemma OAI.CurrentKS.Realization.getD_property line 29
9. lemma OAI.CurrentKS.Realization.zipDefault_property line 36
10. def OAI.CurrentKS.Realization.MatrixParts line 45
11. lemma OAI.CurrentKS.Realization.matrixParts_zero line 46
12. lemma OAI.CurrentKS.Realization.matrixParts_length line 47
13. lemma OAI.CurrentKS.Realization.MatrixParts.mono line 50
14. def OAI.CurrentKS.Realization.MatrixShape line 53
15. lemma OAI.CurrentKS.Realization.matrixShape_length line 54
16. lemma OAI.CurrentKS.Realization.MatrixShape.mono line 58
17. lemma OAI.CurrentKS.Realization.matrix_length_bound line 60
18. lemma OAI.CurrentKS.Realization.accumMatrix_shape line 65
19. lemma OAI.CurrentKS.Realization.accumMatrix_parts line 73
20. lemma OAI.CurrentKS.Realization.accumMatrix_fold line 89
21. instance OAI.CurrentKS.Realization.poly_accumMatrix line 102
22. instance OAI.CurrentKS.Realization.size_accumMatrix line 107
23. instance OAI.CurrentKS.Realization.poly_evalPencil line 127
24. instance OAI.CurrentKS.Realization.poly_normalPencil line 128