OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralOutgoingBasis.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Two canonical normalized slow columns form a rank-two subspace at every exterior point.

  1. theorem OAI.DefocusingNLS.canonical_circular_outgoing_basis line 12
  2. theorem OAI.DefocusingNLS.canonical_holomorphic_circular_basis line 39