OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialModeNoExtraLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Extra actual eigenvalues cannot approach any of the three symmetry values.

  1. theorem OAI.DefocusingNLS.radialMatchedMode_no_extra_limit line 15