OAI/Analysis/MatrixSigning/Realization/SelectionRealization.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CurrentKS.Realization.scoredCode line 15
2. def OAI.CurrentKS.Realization.betterData line 16
3. def OAI.CurrentKS.Realization.better line 18
4. def OAI.CurrentKS.Realization.selectScored line 30
5. lemma OAI.CurrentKS.Realization.selectScored_data line 31
6. lemma OAI.CurrentKS.Realization.select_map line 40
7. def OAI.CurrentKS.Realization.chooseCoordinateData line 48
8. def OAI.CurrentKS.Realization.chooseCoordinate line 50
9. lemma OAI.CurrentKS.Realization.chooseCoordinate_data line 62
10. def OAI.CurrentKS.Realization.gradientDirectionData line 74
11. def OAI.CurrentKS.Realization.gradientDirection line 77
12. lemma OAI.CurrentKS.Realization.gradientDirection_data line 83