OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralRobinRegularity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Continuity and holomorphy of the exact outgoing Robin matrix, on the open set where the value columns are invertible.

  1. theorem OAI.DefocusingNLS.spectralValueDet_tendsto line 11
  2. theorem OAI.DefocusingNLS.spectralValueInverse_tendsto line 16
  3. theorem OAI.DefocusingNLS.spectralRobinOperator_tendsto line 27
  4. theorem OAI.DefocusingNLS.spectralValueInverse_analyticAt line 37
  5. theorem OAI.DefocusingNLS.spectralRobinOperator_analyticAt line 56