OAI/Analysis/MatrixSigning/Realization/FaceChoiceRealization.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CurrentKS.Realization.FaceActive line 13
  2. def OAI.CurrentKS.Realization.activeFaceCode line 14
  3. def OAI.CurrentKS.Realization.faP line 15
  4. def OAI.CurrentKS.Realization.FaceParams.gradient line 17
  5. def OAI.CurrentKS.Realization.FaceParams.hessian line 19
  6. def OAI.CurrentKS.Realization.FaceParams.curvatureParams line 21
  7. def OAI.CurrentKS.Realization.faceCurvatureParams line 23
  8. def OAI.CurrentKS.Realization.FaceParams.curvature line 28
  9. def OAI.CurrentKS.Realization.faceCurvature line 30
  10. def OAI.CurrentKS.Realization.FaceActive.gradientPoint line 33
  11. def OAI.CurrentKS.Realization.faGradientPoint line 37
  12. def OAI.CurrentKS.Realization.vectorSub line 50
  13. lemma OAI.CurrentKS.Realization.vectorSub_data line 51
  14. def OAI.CurrentKS.Realization.curvatureCandidatesData line 54
  15. def OAI.CurrentKS.Realization.curvatureCandidates line 57
  16. lemma OAI.CurrentKS.Realization.curvatureCandidates_data line 62
  17. def OAI.CurrentKS.Realization.FaceActive.candidates line 70
  18. def OAI.CurrentKS.Realization.faCandidates line 74
  19. def OAI.CurrentKS.Realization.FaceActive.choice line 91
  20. def OAI.CurrentKS.Realization.faCandidatePoints line 95
  21. def OAI.CurrentKS.Realization.faChoice line 103