OAI/Analysis/MatrixSigning/Complexity/PolynomialExplicit.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CurrentKS.Realization.PolyTime.then line 14
2. lemma OAI.CurrentKS.Realization.PolyTime.both line 16
3. lemma OAI.CurrentKS.Realization.PolyTime.congr line 18
4. lemma OAI.CurrentKS.Realization.PolyTime.changeOutput line 20
5. lemma OAI.CurrentKS.Realization.PolyTime.ite line 22
6. lemma OAI.CurrentKS.Realization.runsPolyOf line 25
7. lemma OAI.CurrentKS.Realization.PolyTime.mul line 27
8. lemma OAI.CurrentKS.Realization.PolyTime.pow line 30