OAI/MathematicalPhysics/DefocusingNLS/Certificates/ExteriorPolynomialInequalities.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The first two exterior certificate inequalities for the coherent polynomial family.

  1. def OAI.DefocusingNLS.ExteriorCertificate.marginPolynomial line 13
  2. theorem OAI.DefocusingNLS.ExteriorCertificate.margin_sound line 16
  3. def OAI.DefocusingNLS.ExteriorCertificate.realBoundPolynomial line 22
  4. theorem OAI.DefocusingNLS.ExteriorCertificate.realBound_sound line 26
  5. theorem OAI.DefocusingNLS.ExteriorCertificate.margin_degree line 35
  6. theorem OAI.DefocusingNLS.ExteriorCertificate.realBoundPolynomial_degree line 40
  7. theorem OAI.DefocusingNLS.ExteriorCertificate.diagonal_polynomial_positive line 49
  8. theorem OAI.DefocusingNLS.ExteriorCertificate.real_bound_polynomial_positive line 61