OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralRadialCoreLocality.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A radial H¹ vector that vanishes in the core also has zero weak derivative there.

  1. theorem OAI.DefocusingNLS.spectralRadialCore_point_zero_of_le line 10
  2. theorem OAI.DefocusingNLS.spectralRadialCore_derivative_local line 18
  3. theorem OAI.DefocusingNLS.spectralRadialCore_derivative_zero line 38