OAI/MathematicalPhysics/DefocusingNLS/Certificates/ExteriorPositiveEvaluation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Positive coefficient enclosures imply the actual exterior inequalities.

  1. theorem OAI.DefocusingNLS.ExteriorCertificate.positiveCoefficients_get line 12
  2. theorem OAI.DefocusingNLS.ExteriorCertificate.eval_re_eq_sum line 20
  3. theorem OAI.DefocusingNLS.ExteriorCertificate.positive_eval_of_positiveCoefficients line 30