OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralTurningCentralWeight.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The continuous regularized frequency has fixed upper and lower bounds on each scaled Airy interval, uniformly along the escaping sequence.

  1. theorem OAI.DefocusingNLS.spectralTurning_central_weight_bounds line 12