OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralScalarBarrier.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Entry into, and preservation of, a strict scalar differential barrier. This is used for the Airy logarithmic slope.

  1. theorem OAI.DefocusingNLS.spectralScalar_eventually_below line 12
  2. theorem OAI.DefocusingNLS.spectralScalar_eventually_above line 53