OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralRegularLift.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Recovering a regular radial solution and its initial jet from the weighted resolvent.

  1. def OAI.DefocusingNLS.spectralRegularWeight line 13
  2. def OAI.DefocusingNLS.spectralRegularInitial line 22
  3. def OAI.DefocusingNLS.spectralRegularLift line 26
  4. theorem OAI.DefocusingNLS.spectralRegularLift_continuous line 31
  5. theorem OAI.DefocusingNLS.spectralRegularLift_hasDerivAt line 38
  6. theorem OAI.DefocusingNLS.spectralRegularLift_initial line 48
  7. theorem OAI.DefocusingNLS.spectralRegularLift_weighted line 56
  8. theorem OAI.DefocusingNLS.spectralRegularLift_unweight line 74