OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralRobinMatrix.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The outgoing Robin operator obtained from two value/derivative columns. Only the nonzero value determinant is needed for the local construction.

  1. def OAI.DefocusingNLS.spectralTwoColumns line 12
  2. def OAI.DefocusingNLS.spectralValueDet line 16
  3. def OAI.DefocusingNLS.spectralValueInverse line 18
  4. def OAI.DefocusingNLS.spectralRobinOperator line 21
  5. theorem OAI.DefocusingNLS.spectralTwoColumns_apply line 24
  6. theorem OAI.DefocusingNLS.spectralValueInverse_apply_columns line 27
  7. theorem OAI.DefocusingNLS.spectralRobinOperator_columns line 42
  8. theorem OAI.DefocusingNLS.spectralTwoColumns_tendsto line 47
  9. theorem OAI.DefocusingNLS.spectralTwoColumns_analyticAt line 55