OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralOutgoingBoundary.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Actual outgoing columns have invertible value matrices at large radius, in addition to solving the physical equation and depending holomorphically.

  1. theorem OAI.DefocusingNLS.canonical_physical_boundary_basis line 13