OAI/Analysis/MatrixSigning/Complexity/PolynomialArrays.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CurrentKS.Realization.fold_add_eq line 15
2. lemma OAI.CurrentKS.Realization.rat_sum_lengths_le line 19
3. instance OAI.CurrentKS.Realization.size_ratAdd line 27
4. instance OAI.CurrentKS.Realization.poly_sumRationals line 40
5. instance OAI.CurrentKS.Realization.poly_l1Rationals line 43
6. instance OAI.CurrentKS.Realization.poly_lookupStep line 45
7. lemma OAI.CurrentKS.Realization.lookup_fold_size line 48
8. instance OAI.CurrentKS.Realization.size_lookupStep line 65
9. instance OAI.CurrentKS.Realization.poly_getD line 79
10. instance OAI.CurrentKS.Realization.poly_zipWith line 81
11. instance OAI.CurrentKS.Realization.poly_vectorAdd line 83
12. instance OAI.CurrentKS.Realization.poly_vectorScaleBody line 84
13. instance OAI.CurrentKS.Realization.poly_vectorScale line 85
14. instance OAI.CurrentKS.Realization.poly_matrixAdd line 86
15. instance OAI.CurrentKS.Realization.poly_matrixScale line 87
16. instance OAI.CurrentKS.Realization.poly_dot line 88
17. instance OAI.CurrentKS.Realization.poly_matVec line 89
18. instance OAI.CurrentKS.Realization.poly_quadratic line 90
19. lemma OAI.CurrentKS.Realization.ratLength_natCast line 92
20. instance OAI.CurrentKS.Realization.size_ratSucc line 96
21. instance OAI.CurrentKS.Realization.poly_natToRat line 105
22. instance OAI.CurrentKS.Realization.size_natMulStep line 106
23. instance OAI.CurrentKS.Realization.poly_natMul line 115