OAI/MathematicalPhysics/DefocusingNLS/Certificates/BoundaryCertificateSemantics.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Soundness of the boundary coefficient recipe

  1. theorem OAI.DefocusingNLS.GaussianEnclosure.realPart_pos line 12
  2. theorem OAI.DefocusingNLS.GaussianEnclosure.realPart_sound line 20
  3. theorem OAI.DefocusingNLS.BoundaryCertificate.constant_sound line 36
  4. theorem OAI.DefocusingNLS.BoundaryCertificate.sharpPolynomial_cons line 40
  5. theorem OAI.DefocusingNLS.BoundaryCertificate.sharpAux_sound line 47
  6. theorem OAI.DefocusingNLS.BoundaryCertificate.sharp_sound line 67
  7. theorem OAI.DefocusingNLS.BoundaryCertificate.symmetrize_sound line 71
  8. theorem OAI.DefocusingNLS.BoundaryCertificate.hermitian_sound line 76