OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralRemotePhysicalOperator.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Separation of the actual Euler eigenpair system into its leading and bounded parts.

  1. def OAI.DefocusingNLS.spectralRemotePositionPlus line 11
  2. def OAI.DefocusingNLS.spectralRemotePositionMinus line 13
  3. def OAI.DefocusingNLS.spectralRemoteVelocityPlus line 15
  4. def OAI.DefocusingNLS.spectralRemoteVelocityMinus line 17
  5. def OAI.DefocusingNLS.spectralRemoteBoundedOperator line 20
  6. theorem OAI.DefocusingNLS.spectralRemoteBoundedOperator_apply line 28
  7. def OAI.DefocusingNLS.spectralRemotePhysicalBounded line 32
  8. theorem OAI.DefocusingNLS.spectralRemoteEulerField_operator line 36