OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialAngularScalar.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Adding a spherical-harmonic eigenvalue to the regular scalar spectral forms.

  1. def OAI.DefocusingNLS.radialAngularScalarAction line 12
  2. def OAI.DefocusingNLS.radialAngularScalarForm line 16
  3. def OAI.DefocusingNLS.radialAngularScalarVirial line 20
  4. def OAI.DefocusingNLS.radialAngularScalarBoundary line 24
  5. theorem OAI.DefocusingNLS.radialAngularScalarForm_symm line 28
  6. theorem OAI.DefocusingNLS.radialAngularScalarAction_continuousOn line 34
  7. theorem OAI.DefocusingNLS.radialAngularScalarForm_spectralTest_boundary line 43