OAI/MathematicalPhysics/DefocusingNLS/Certificates/ExteriorCertificateRecipe.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The depth-five exterior certificate with a free real spatial variable.

  1. def OAI.DefocusingNLS.ExteriorCertificate.step line 11
  2. def OAI.DefocusingNLS.ExteriorCertificate.state line 21
  3. def OAI.DefocusingNLS.ExteriorCertificate.hermitian line 25
  4. def OAI.DefocusingNLS.ExteriorCertificate.diagonal line 32
  5. def OAI.DefocusingNLS.ExteriorCertificate.lowerOffDiagonal line 36
  6. def OAI.DefocusingNLS.ExteriorCertificate.realCoefficients line 40
  7. def OAI.DefocusingNLS.ExteriorCertificate.negImagCoefficients line 45
  8. def OAI.DefocusingNLS.ExteriorCertificate.determinantMargin line 50
  9. def OAI.DefocusingNLS.ExteriorCertificate.realBound line 54
  10. def OAI.DefocusingNLS.ExteriorCertificate.imaginaryBound line 60
  11. def OAI.DefocusingNLS.ExteriorCertificate.positiveCoefficients line 64