OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralCircularSource.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Bounded coupled source fields for the two circular tail equations.

  1. theorem OAI.DefocusingNLS.circularSource_bound line 11
  2. def OAI.DefocusingNLS.boundedCircularSource line 24
  3. theorem OAI.DefocusingNLS.boundedCircularSource_evaluation line 36
  4. theorem OAI.DefocusingNLS.boundedCircularSource_norm line 43
  5. theorem OAI.DefocusingNLS.boundedCircularSource_difference line 55