OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralCircularField.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The actual bounded part of the rescaled two-channel spectral system.

  1. def OAI.DefocusingNLS.circularBoundedField line 11
  2. def OAI.DefocusingNLS.circularFieldBound line 17
  3. theorem OAI.DefocusingNLS.spectralDiagonalCoefficient_norm line 21
  4. theorem OAI.DefocusingNLS.spectralCrossCoefficient_norm line 33
  5. theorem OAI.DefocusingNLS.circularBoundedField_zero line 45
  6. theorem OAI.DefocusingNLS.circularBoundedField_sub line 49
  7. theorem OAI.DefocusingNLS.circularBoundedField_continuous line 55