OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialMatchedCompactExclusion.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Compact subsets disjoint from the free outgoing zeros eventually contain no actual radial eigenvalues. The matching equations determine the limiting profile internally.

  1. theorem OAI.DefocusingNLS.radialMatchedSpectralMode_limit_zero_of_matching line 15
  2. theorem OAI.DefocusingNLS.radialMatchedSpectralMode_compact_exclusion line 36