OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralSimpleKernelEstimate.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The estimate on a fixed complement of a simple compact-pencil kernel. This is the quantitative input for excluding nearby additional roots.

  1. theorem OAI.DefocusingNLS.compact_approximate_kernel_limit line 11
  2. theorem OAI.DefocusingNLS.compact_simple_kernel_estimate line 32
  3. theorem OAI.DefocusingNLS.kernel_complement_perturbation_estimate line 85
  4. theorem OAI.DefocusingNLS.kernel_unique_with_normalization line 101