OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousSpectralLocalizationRemote.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The two remote leading eigenvectors have a uniform gap. The scalar c is the actual combination h * omega / r² + ell * (ell + 10) / r⁴.

  1. def OAI.DefocusingNLS.homogeneousSpectralLocalizationRemoteRoot line 11
  2. def OAI.DefocusingNLS.homogeneousSpectralLocalizationRemoteField line 14
  3. theorem OAI.DefocusingNLS.homogeneousSpectralLocalizationRemoteRoot_equation line 18
  4. theorem OAI.DefocusingNLS.homogeneousSpectralLocalizationRemoteField_eigenvector line 35
  5. theorem OAI.DefocusingNLS.homogeneousSpectralLocalizationRemoteRoot_gap line 47
  6. theorem OAI.DefocusingNLS.homogeneousSpectralLocalizationRemoteRoot_uniform line 63
  7. theorem OAI.DefocusingNLS.homogeneousSpectralLocalizationRemoteRoot_norm line 83
  8. theorem OAI.DefocusingNLS.homogeneousSpectralLocalizationRemoteFrame_bounds line 103
  9. theorem OAI.DefocusingNLS.homogeneousSpectralLocalizationRemote_coefficient line 130
  10. theorem OAI.DefocusingNLS.homogeneousSpectralLocalizationRemote_actual_gap line 160