OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralTurningRootConstruction.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Explicit construction of the unique positive turning radius and its Airy scale for the actual radial frequency.

  1. def OAI.DefocusingNLS.spectralTurningRoot line 12
  2. theorem OAI.DefocusingNLS.spectralTurningRoot_data line 15
  3. def OAI.DefocusingNLS.spectralTurningRootScale line 45
  4. theorem OAI.DefocusingNLS.spectralTurningRootScale_data line 48