OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialSpectralEnergyPositive.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Every nonzero regular radial eigenpair has strictly positive physical H1/angular energy on every ball of positive radius.

  1. theorem OAI.DefocusingNLS.harmonicRadialEigenpair_energy_pos line 12