OAI/Geometry/PrescribedPotential/NonlinearHessianCommutator.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Nonlinear Hessian Commutator.

  1. lemma OAI.NonlinearHessian.determinant_contDiff line 22
  2. def OAI.NonlinearHessian.detDifferential line 32
  3. lemma OAI.NonlinearHessian.detDifferential_hasFDeriv line 35
  4. def OAI.NonlinearHessian.hessianMatrix line 39
  5. lemma OAI.NonlinearHessian.hessianMatrix_contDiff line 42
  6. lemma OAI.NonlinearHessian.hessianMatrix_fderiv line 49
  7. def OAI.NonlinearHessian.complexCutoff line 63
  8. lemma OAI.NonlinearHessian.complexCutoff_apply line 66
  9. def OAI.NonlinearHessian.cutoffHessianError line 69
  10. lemma OAI.NonlinearHessian.hessianMatrix_cutoff line 72
  11. lemma OAI.NonlinearHessian.determinant_cutoff_commutator line 89