OAI/Analysis/MatrixSigning/Realization/PencilArrayRealization.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CurrentKS.Realization.PencilData line 13
2. abbrev OAI.CurrentKS.Realization.pencilCode line 14
3. def OAI.CurrentKS.Realization.accumMatrix line 16
4. def OAI.CurrentKS.Realization.accumMatrixRealizes line 20
5. def OAI.CurrentKS.Realization.evalPencilData line 25
6. def OAI.CurrentKS.Realization.evalPencil line 29
7. def OAI.CurrentKS.Realization.normalData line 37
8. def OAI.CurrentKS.Realization.normalPencil line 40
9. def OAI.CurrentKS.Realization.pencilData line 45
10. lemma OAI.CurrentKS.Realization.accumMatrix_data line 48
11. lemma OAI.CurrentKS.Realization.fold_matrixData line 53
12. lemma OAI.CurrentKS.Realization.evalPencil_data line 63
13. lemma OAI.CurrentKS.Realization.normalPencil_data line 74