OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralFirstTest.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The first scalar equation can be tested outside the constrained core.

  1. def OAI.DefocusingNLS.spectralFirstTest line 11
  2. theorem OAI.DefocusingNLS.spectralFirstTest_core line 16
  3. theorem OAI.DefocusingNLS.spectralFirstTest_values line 26
  4. theorem OAI.DefocusingNLS.spectralFirstTest_derivatives line 33
  5. theorem OAI.DefocusingNLS.spectralFirstTest_traces line 40
  6. theorem OAI.DefocusingNLS.spectralFirstTest_equation line 46