OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialAngularForms.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The angular part of the radial spectral form and its exact testing identity.

  1. def OAI.DefocusingNLS.radialAngularForm line 12
  2. def OAI.DefocusingNLS.radialAngularVirial line 16
  3. def OAI.DefocusingNLS.radialAngularBoundary line 21
  4. theorem OAI.DefocusingNLS.radialAngularForm_diag line 25
  5. theorem OAI.DefocusingNLS.radialAngularForm_symm line 32
  6. theorem OAI.DefocusingNLS.radialAngularForm_nonneg line 39
  7. theorem OAI.DefocusingNLS.radialAngularForm_spectralTest line 48