OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralFrameAmplitude.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Terminal normalization bounds the coefficient of a single WKB branch above and below when its real action is bounded.

  1. theorem OAI.DefocusingNLS.spectralFrame_amplitude_bounds line 10
  2. theorem OAI.DefocusingNLS.spectralScalarFlux_smul line 32