OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousGeneratorCoordinates.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Finite generator eigenvectors in the actual evolution domain

An eigenvector on the finite contour space evolves by its scalar exponential. Its two real coordinates therefore belong to the free generator domain and satisfy the exact bounded-potential equations.

  1. theorem OAI.DefocusingNLS.projectionSemigroup_eigenvector line 28
  2. theorem OAI.DefocusingNLS.hasDerivWithinAt_semigroup_eigenvector line 42
  3. theorem OAI.DefocusingNLS.homogeneous_eigenvector_free_coordinates line 68