OAI/Analysis/MatrixSigning/Complexity/PolynomialFamilies.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CurrentKS.Realization.IsPoly line 15
2. lemma OAI.CurrentKS.Realization.IsPoly.mono line 16
3. lemma OAI.CurrentKS.Realization.IsPoly.add line 19
4. lemma OAI.CurrentKS.Realization.IsPoly.mul line 22
5. lemma OAI.CurrentKS.Realization.IsPoly.pow line 25
6. lemma OAI.CurrentKS.Realization.isPoly_const line 28
7. lemma OAI.CurrentKS.Realization.isPoly_self line 29
8. lemma OAI.CurrentKS.Realization.IsPoly.eval line 30
9. lemma OAI.CurrentKS.Realization.IsPoly.reindex line 33
10. lemma OAI.CurrentKS.Realization.isPoly_pair line 36
11. structure OAI.CurrentKS.Realization.RunsPoly line 43
12. lemma OAI.CurrentKS.Realization.RunsPoly.of_poly line 46
13. lemma OAI.CurrentKS.Realization.RunsPoly.output line 51
14. lemma OAI.CurrentKS.Realization.RunsPoly.then line 53
15. lemma OAI.CurrentKS.Realization.RunsPoly.then_poly line 56
16. lemma OAI.CurrentKS.Realization.RunsPoly.both line 59
17. lemma OAI.CurrentKS.Realization.RunsPoly.congr line 68
18. lemma OAI.CurrentKS.Realization.RunsPoly.changeOutput line 73
19. lemma OAI.CurrentKS.Realization.RunsPoly.reindex line 76
20. lemma OAI.CurrentKS.Realization.Realizes.congr_cost line 81
21. lemma OAI.CurrentKS.Realization.RunsPoly.ite line 86