OAI/Analysis/MatrixSigning/Realization/StencilRealization.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentKS.Realization.vectorNeg line 14
  2. lemma OAI.CurrentKS.Realization.vectorNeg_ofFn line 16
  3. lemma OAI.CurrentKS.Realization.vectorScale_ofFn line 18
  4. def OAI.CurrentKS.Realization.stencilAt line 21
  5. abbrev OAI.CurrentKS.Realization.FaceIndex line 38
  6. abbrev OAI.CurrentKS.Realization.faceIndexCode line 39
  7. def OAI.CurrentKS.Realization.fiP line 40
  8. def OAI.CurrentKS.Realization.fiI line 41
  9. def OAI.CurrentKS.Realization.fiBasis line 42
  10. def OAI.CurrentKS.Realization.stencilGradientEntry line 46
  11. def OAI.CurrentKS.Realization.stencilGradient line 54
  12. abbrev OAI.CurrentKS.Realization.FaceDouble line 59
  13. abbrev OAI.CurrentKS.Realization.faceDoubleCode line 60
  14. def OAI.CurrentKS.Realization.fdS line 61
  15. def OAI.CurrentKS.Realization.fdP line 62
  16. def OAI.CurrentKS.Realization.fdI line 63
  17. def OAI.CurrentKS.Realization.fdJ line 64
  18. def OAI.CurrentKS.Realization.fdBasisI line 65
  19. def OAI.CurrentKS.Realization.fdBasisJ line 66
  20. def OAI.CurrentKS.Realization.stencilHessianEntry line 70
  21. def OAI.CurrentKS.Realization.stencilHessianRow line 105
  22. def OAI.CurrentKS.Realization.stencilHessian line 106