OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralCompactChainLimit.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Divided differences of normalized pencil eigenvectors produce an actual first chain in the compact limit.

  1. theorem OAI.DefocusingNLS.compact_variable_forced_limit line 14
  2. theorem OAI.DefocusingNLS.compact_complement_forced_limit line 36
  3. theorem OAI.DefocusingNLS.pencil_divided_difference_equation line 58
  4. theorem OAI.DefocusingNLS.compact_pencil_no_splitting line 65