OAI/MathematicalPhysics/DefocusingNLS/Certificates/BoundaryHermitianPolynomial.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Hermitian polynomial and its reflected boundary sum

  1. def OAI.DefocusingNLS.conjugatePolynomial line 12
  2. def OAI.DefocusingNLS.sharpPolynomial line 15
  3. theorem OAI.DefocusingNLS.coeff_conjugatePolynomial line 18
  4. theorem OAI.DefocusingNLS.coeff_sharpPolynomial line 22
  5. theorem OAI.DefocusingNLS.conjugatePolynomial_degree line 26
  6. theorem OAI.DefocusingNLS.sharpPolynomial_degree line 29
  7. def OAI.DefocusingNLS.hermitianPolynomial line 35
  8. theorem OAI.DefocusingNLS.hermitianPolynomial_degree line 40
  9. theorem OAI.DefocusingNLS.hermitianPolynomial_top line 54
  10. def OAI.DefocusingNLS.reflectedHermitianPolynomial line 67
  11. theorem OAI.DefocusingNLS.reflectedHermitianPolynomial_degree line 71
  12. theorem OAI.DefocusingNLS.reflectedHermitianPolynomial_coefficient line 78