OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralTurningConeError.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The error threshold for the forbidden WKB cone follows from the actual residual integral and action, with the fixed cutoff chosen first.

  1. theorem OAI.DefocusingNLS.spectralTurning_eventual_cone_error line 13
  2. theorem OAI.DefocusingNLS.spectralTurning_eventual_relative_error line 85