OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralCaseIIComparisons.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual frequency-dominated geometry constructs the mixed pair; no turning radius or Airy scale is assumed.

  1. theorem OAI.DefocusingNLS.spectralCaseII_comparisons line 11