OAI/Analysis/MatrixSigning/Realization/CurvatureRealization.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentKS.Realization.squareSumData line 12
  2. def OAI.CurrentKS.Realization.squareSum line 13
  3. lemma OAI.CurrentKS.Realization.squareSum_data line 14
  4. def OAI.CurrentKS.Realization.vectorDivide line 17
  5. def OAI.CurrentKS.Realization.initialScaleData line 21
  6. def OAI.CurrentKS.Realization.initialScale line 22
  7. lemma OAI.CurrentKS.Realization.initialScale_data line 24
  8. def OAI.CurrentKS.Realization.normalizeData line 29
  9. def OAI.CurrentKS.Realization.normalizeVector line 32
  10. lemma OAI.CurrentKS.Realization.normalize_data line 37
  11. def OAI.CurrentKS.Realization.intCeil line 41
  12. def OAI.CurrentKS.Realization.nearest line 43
  13. def OAI.CurrentKS.Realization.nearestMesh line 49
  14. def OAI.CurrentKS.Realization.roundMesh line 53
  15. lemma OAI.CurrentKS.Realization.roundMesh_data line 54
  16. structure OAI.CurrentKS.Realization.CurvatureParams line 60
  17. abbrev OAI.CurrentKS.Realization.curvatureDataCode line 67
  18. def OAI.CurrentKS.Realization.CurvatureParams.data line 68
  19. def OAI.CurrentKS.Realization.curvatureCode line 69
  20. def OAI.CurrentKS.Realization.curvatureView line 70
  21. def OAI.CurrentKS.Realization.cuN line 72
  22. def OAI.CurrentKS.Realization.cuRest line 73
  23. def OAI.CurrentKS.Realization.cuH line 74
  24. def OAI.CurrentKS.Realization.cuScalars line 75
  25. def OAI.CurrentKS.Realization.cuA line 76
  26. def OAI.CurrentKS.Realization.cuMore line 77
  27. def OAI.CurrentKS.Realization.cuM line 78
  28. def OAI.CurrentKS.Realization.cuLast line 79
  29. def OAI.CurrentKS.Realization.cuS line 80
  30. def OAI.CurrentKS.Realization.cuRho line 81
  31. def OAI.CurrentKS.Realization.cuShift line 83
  32. def OAI.CurrentKS.Realization.computedCurvature line 97