OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralRemoteOutgoingSymbol.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Canonical outgoing columns give individual logarithmic symbols for the actual harmonic eigenpair coordinates.

  1. theorem OAI.DefocusingNLS.spectralRemote_physical_value_symbol line 14
  2. theorem OAI.DefocusingNLS.spectralRemote_outgoing_span_symbol line 27