OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralPowerPressureAway.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The exterior small-pressure hypothesis follows from subunit amplitude convergence. The scale is the reciprocal of the nonlinear exponent.

  1. theorem OAI.DefocusingNLS.spectralPower_pressure_away line 13