OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialSpectralStripBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Exclusion of escaping mode sequences gives a uniform angular/frequency bound for all sufficiently large matched powers in the counting strip.

  1. theorem OAI.DefocusingNLS.radialMatchedSpectralMode_strip_bound line 12