OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralTurningCoefficient.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual complex Liouville coefficient converges to the Airy coefficient on each fixed rescaled interval, with an explicit uniform error.

  1. def OAI.DefocusingNLS.spectralTurningCoefficient line 11
  2. theorem OAI.DefocusingNLS.spectralTurningCoefficient_bound line 16