OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralRemoteExteriorGrowth.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Coarse derivative growth and then all uniform logarithmic jets for the actual canonical nonlinear exterior profile. No derivative bounds are assumed.

  1. theorem OAI.DefocusingNLS.spectralRemote_exterior_uniform_growth line 14
  2. theorem OAI.DefocusingNLS.spectralRemote_exterior_uniform_symbol line 52