OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralCutoffProfile.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Smooth cutoffs with a fixed derivative bound after rescaling the collar.

  1. theorem OAI.DefocusingNLS.spectralTransition_fderiv_zero line 13
  2. theorem OAI.DefocusingNLS.spectralTransition_fderiv_compact line 25
  3. theorem OAI.DefocusingNLS.spectralTransition_temperate line 29
  4. theorem OAI.DefocusingNLS.spectralTransition_deriv_bound line 39
  5. def OAI.DefocusingNLS.spectralCollarCutoff line 54
  6. def OAI.DefocusingNLS.spectralCollarCutoffDerivative line 57
  7. theorem OAI.DefocusingNLS.spectralCollarCutoff_hasDerivAt line 60
  8. theorem OAI.DefocusingNLS.spectralCollarCutoff_temperate line 69
  9. theorem OAI.DefocusingNLS.spectralCollarCutoff_zero line 77
  10. theorem OAI.DefocusingNLS.spectralCollarCutoff_one line 82
  11. theorem OAI.DefocusingNLS.spectralCollarCutoff_bounds line 87
  12. theorem OAI.DefocusingNLS.spectralCollarCutoffDerivative_bound line 91