OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralRemoteMatrixOperator.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The exact matrix realization of the four remote coordinates.

  1. def OAI.DefocusingNLS.spectralRemoteIndexEquiv line 13
  2. def OAI.DefocusingNLS.spectralRemoteBasis line 19
  3. def OAI.DefocusingNLS.spectralRemoteMatrixEquiv line 22
  4. def OAI.DefocusingNLS.spectralRemoteMatrixOperator line 27
  5. theorem OAI.DefocusingNLS.spectralRemoteMatrixOperator_add line 31
  6. theorem OAI.DefocusingNLS.spectralRemoteMatrixOperator_smul line 35
  7. theorem OAI.DefocusingNLS.spectralRemoteMatrixOperator_mul line 39
  8. theorem OAI.DefocusingNLS.spectralRemoteMatrixOperator_sub line 43
  9. def OAI.DefocusingNLS.spectralRemoteMatrixOperatorL line 47
  10. def OAI.DefocusingNLS.spectralRemoteOperatorMatrix line 51
  11. theorem OAI.DefocusingNLS.spectralRemoteMatrixOperator_inverse line 54
  12. theorem OAI.DefocusingNLS.spectralRemoteOperatorMatrix_inverse line 58