OAI/Analysis/KLS/Stein/SteinHessianDefs.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LeanBlast.KLS.standardBasisVector line 15
  2. def OAI.LeanBlast.KLS.partialDerivative line 18
  3. def OAI.LeanBlast.KLS.hessianMatrix line 21
  4. def OAI.LeanBlast.KLS.hessianSlice line 25
  5. def OAI.LeanBlast.KLS.matrixHSNormSq line 29
  6. def OAI.LeanBlast.KLS.steinGenerator line 32
  7. def OAI.LeanBlast.KLS.steinGamma line 36
  8. def OAI.LeanBlast.KLS.steinQ line 39
  9. def OAI.LeanBlast.KLS.steinHessianEnergy line 44
  10. theorem OAI.LeanBlast.KLS.hessianMatrix_isSymm line 48
  11. theorem OAI.LeanBlast.KLS.matrixHSNormSq_nonneg line 54
  12. theorem OAI.LeanBlast.KLS.matrixHSNormSq_eq_trace_sq line 58