OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousSymmetryEvolution.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The physical phase, translation and time directions are actual eigenvectors

  1. theorem OAI.DefocusingNLS.symbol line 37
  2. theorem OAI.DefocusingNLS.radialMatched_phase_evolution line 45
  3. theorem OAI.DefocusingNLS.radialMatched_translation_evolution line 60
  4. theorem OAI.DefocusingNLS.radialMatched_time_evolution line 74