OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralTurningProjectionIdentity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact identification of the rescaled growing projection with the physical WKB coefficient at the forbidden endpoint.

  1. theorem OAI.DefocusingNLS.spectralTurning_sqrt_momentum_scale line 11
  2. theorem OAI.DefocusingNLS.spectralTurning_projection_identity line 17
  3. theorem OAI.DefocusingNLS.spectralTurning_projection_norm_scale line 36