OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralTurningOuterWeight.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Monotonicity of the actual frequency identifies the regularized norm with the WKB norm on each outer interval.

  1. theorem OAI.DefocusingNLS.spectralTurningRegularizedWeight_left line 12
  2. theorem OAI.DefocusingNLS.spectralTurningRegularizedWeight_right line 28
  3. theorem OAI.DefocusingNLS.spectralTurningCoefficient_real_error line 42
  4. theorem OAI.DefocusingNLS.spectralTurning_regularized_outer_weights line 51