OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralThreeRegionGreen.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Extend the Dirichlet/outgoing construction across a turning interval and the oscillatory region. No exponential comparison between channels is needed.

  1. theorem OAI.DefocusingNLS.spectralScalar_three_region_green_and_extension line 13
  2. theorem OAI.DefocusingNLS.spectralScalar_three_region_green line 75