OAI/Analysis/MatrixSigning/Realization/FaceQueryRealization.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.CurrentKS.Realization.FaceParams line 14
  2. abbrev OAI.CurrentKS.Realization.faceDataCode line 21
  3. def OAI.CurrentKS.Realization.FaceParams.data line 22
  4. def OAI.CurrentKS.Realization.faceCode line 25
  5. def OAI.CurrentKS.Realization.faceView line 26
  6. def OAI.CurrentKS.Realization.fD line 28
  7. def OAI.CurrentKS.Realization.fRest line 29
  8. def OAI.CurrentKS.Realization.fAtoms line 30
  9. def OAI.CurrentKS.Realization.fArgs line 31
  10. def OAI.CurrentKS.Realization.fBase line 32
  11. def OAI.CurrentKS.Realization.fScalars line 34
  12. def OAI.CurrentKS.Realization.fNu line 35
  13. def OAI.CurrentKS.Realization.fLam line 36
  14. def OAI.CurrentKS.Realization.fIndices line 37
  15. abbrev OAI.CurrentKS.Realization.FaceParams.n line 40
  16. def OAI.CurrentKS.Realization.fN line 41
  17. def OAI.CurrentKS.Realization.FaceParams.schedule line 43
  18. def OAI.CurrentKS.Realization.fSchedule line 44
  19. def OAI.CurrentKS.Realization.gatherData line 47
  20. def OAI.CurrentKS.Realization.gather line 48
  21. lemma OAI.CurrentKS.Realization.gather_data line 50
  22. def OAI.CurrentKS.Realization.fState line 53
  23. structure OAI.CurrentKS.Realization.FacePoint line 56
  24. def OAI.CurrentKS.Realization.facePointData line 59
  25. def OAI.CurrentKS.Realization.facePointCode line 60
  26. def OAI.CurrentKS.Realization.facePointView line 61
  27. def OAI.CurrentKS.Realization.fpP line 63
  28. def OAI.CurrentKS.Realization.fpY line 64
  29. def OAI.CurrentKS.Realization.fpExtend line 65
  30. def OAI.CurrentKS.Realization.FacePoint.potential line 69
  31. def OAI.CurrentKS.Realization.fpPotential line 73
  32. def OAI.CurrentKS.Realization.faceQuery line 80
  33. def OAI.CurrentKS.Realization.faceStencil line 84
  34. def OAI.CurrentKS.Realization.faceScore line 89