OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialJordanMode.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A nontrivial classical radial Jordan pair with the actual finite-energy conditions.

  1. def OAI.DefocusingNLS.HasRadialJordanMode line 12
  2. theorem OAI.DefocusingNLS.HasRadialJordanMode.radialMode line 23