OAI/Geometry/PrescribedPotential/ComplexHessian.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Complex Hessian.

  1. lemma OAI.SobolevChart.schwartzCoord_smul line 19
  2. lemma OAI.SobolevChart.CoreBound.smul line 25
  3. lemma OAI.SobolevChart.complex_smooth_second_deriv line 33
  4. lemma OAI.GlobalElliptic.second_postcomp_general line 43
  5. def OAI.GlobalElliptic.hessianDirection line 58
  6. def OAI.GlobalElliptic.hessianIDirection line 59
  7. def OAI.GlobalElliptic.hessianEntrySchwartz line 61
  8. lemma OAI.GlobalElliptic.hessianEntrySchwartz_apply line 72
  9. lemma OAI.GlobalElliptic.hessianEntrySchwartz_bound line 83
  10. lemma OAI.GlobalElliptic.hessianEntrySchwartz_real line 90