OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralCoreTestDensity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Tests separated from the pressure core are dense in its constrained harmonic domain.

  1. theorem OAI.DefocusingNLS.spectralHarmonicCutoff_core_zero line 11
  2. theorem OAI.DefocusingNLS.spectralHarmonicCore_test_dense line 26