OAI/Analysis/MatrixSigning/Realization/RootRealization.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CurrentKS.Realization.rootStateCode line 13
2. def OAI.CurrentKS.Realization.rootStep line 14
3. def OAI.CurrentKS.Realization.rootStepRealizes line 17
4. lemma OAI.CurrentKS.Realization.square_iterate line 26
5. lemma OAI.CurrentKS.Realization.cube_iterate line 31
6. def OAI.CurrentKS.Realization.rootRun line 37
7. def OAI.CurrentKS.Realization.upperSqrt line 45
8. def OAI.CurrentKS.Realization.approxPsi line 53