OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralOscillatoryWeight.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The complex momentum weight and the real outgoing normalization are uniformly comparable at a positive-frequency remote endpoint.

  1. theorem OAI.DefocusingNLS.spectralComplexSqrt_weight_comparable line 11
  2. theorem OAI.DefocusingNLS.spectralOscillatoryData_complex_norm line 30