OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralFieldOperator.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Complex-linear coefficient operators and their polynomial dependence on the spectral parameter.

  1. def OAI.DefocusingNLS.circularFieldBounded line 12
  2. theorem OAI.DefocusingNLS.circularFieldBounded_evaluation line 23
  3. theorem OAI.DefocusingNLS.circularFieldBounded_norm line 28
  4. def OAI.DefocusingNLS.circularFieldOperator line 43
  5. theorem OAI.DefocusingNLS.circularFieldOperator_evaluation line 71
  6. theorem OAI.DefocusingNLS.circularFieldOperator_norm line 76