OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralRemoteBlocks.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The four-coordinate off-block Sylvester equation. The outgoing two-plane is kept intact, so no separation is required between its two eigenvalues.

  1. abbrev OAI.DefocusingNLS.SpectralRemoteIndex line 12
  2. def OAI.DefocusingNLS.spectralRemoteBlock line 14
  3. def OAI.DefocusingNLS.spectralRemoteBlockPart line 17
  4. def OAI.DefocusingNLS.spectralRemoteOffChange line 22
  5. theorem OAI.DefocusingNLS.spectralRemote_sylvester line 28
  6. theorem OAI.DefocusingNLS.spectralRemote_off_change_bound line 44