OAI/Analysis/MatrixSigning/Realization/ScheduleRealization.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentKS.Realization.Realizes.min line 14
  2. def OAI.CurrentKS.Realization.Realizes.max line 17
  3. def OAI.CurrentKS.Realization.Realizes.inv line 20
  4. def OAI.CurrentKS.Realization.Realizes.eq line 22
  5. abbrev OAI.CurrentKS.Realization.scheduleArgsCode line 31
  6. def OAI.CurrentKS.Realization.saD line 32
  7. def OAI.CurrentKS.Realization.saRest line 33
  8. def OAI.CurrentKS.Realization.saN line 34
  9. def OAI.CurrentKS.Realization.saScalars line 35
  10. def OAI.CurrentKS.Realization.saNu line 36
  11. def OAI.CurrentKS.Realization.saLam line 37
  12. def OAI.CurrentKS.Realization.saEpsilon line 38
  13. def OAI.CurrentKS.Realization.saSigma line 39
  14. def OAI.CurrentKS.Realization.movementBudget line 41
  15. def OAI.CurrentKS.Realization.saThreshold line 50
  16. def OAI.CurrentKS.Realization.saCoarse line 54
  17. def OAI.CurrentKS.Realization.saCurve2 line 62
  18. def OAI.CurrentKS.Realization.saCurve3 line 70
  19. def OAI.CurrentKS.Realization.saBudget line 81
  20. def OAI.CurrentKS.Realization.saStep line 85
  21. def OAI.CurrentKS.Realization.saStencil line 88
  22. def OAI.CurrentKS.Realization.saMesh line 91
  23. def OAI.CurrentKS.Realization.parametersData line 94
  24. def OAI.CurrentKS.Realization.parametersCode line 95
  25. def OAI.CurrentKS.Realization.parameters line 97
  26. def OAI.CurrentKS.Realization.parameterField line 112