OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralRadialCoreSpace.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The fixed-harmonic energy pair and its closed constrained core domain.

  1. instance OAI.DefocusingNLS.spectralRadialEnergy_realInner line 11
  2. abbrev OAI.DefocusingNLS.SpectralRadialPairEnergy line 15
  3. def OAI.DefocusingNLS.spectralRadialFirstValue line 18
  4. def OAI.DefocusingNLS.spectralRadialPairTrace line 23
  5. theorem OAI.DefocusingNLS.spectralRadialPairTrace_compact line 30
  6. theorem OAI.DefocusingNLS.coreIndicator_measurable line 34
  7. theorem OAI.DefocusingNLS.coreIndicator_bound line 38
  8. def OAI.DefocusingNLS.spectralRadialCoreMask line 44
  9. theorem OAI.DefocusingNLS.spectralRadialCoreMask_zero line 49
  10. def OAI.DefocusingNLS.spectralRadialCoreSubspace line 72
  11. abbrev OAI.DefocusingNLS.SpectralRadialCoreEnergy line 76
  12. instance OAI.DefocusingNLS.spectralRadialCoreEnergy_complete line 78
  13. theorem OAI.DefocusingNLS.spectralRadialCoreSubspace_mem line 83