OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialStationaryReconstruction.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The coupled positive inner amplitude reconstructs an actual complex stationary solution.

  1. def OAI.DefocusingNLS.radialInnerPhase line 12
  2. def OAI.DefocusingNLS.radialInnerComplex line 15
  3. theorem OAI.DefocusingNLS.radialInnerComplex_stationary line 18
  4. theorem OAI.DefocusingNLS.radialInnerComplex_origin line 74
  5. theorem OAI.DefocusingNLS.radialInnerComplex_norm line 79