OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialMatchedSimpleKernel.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The concrete free compact pencil has a quantitative lower bound on every fixed complement of a nonzero kernel vector.

  1. def OAI.DefocusingNLS.radialMatchedFreeBoundary line 14
  2. def OAI.DefocusingNLS.radialMatchedFreePencil line 23
  3. theorem OAI.DefocusingNLS.radialMatchedFreePencil_kernel_line line 32
  4. theorem OAI.DefocusingNLS.radialMatchedFreePencil_complement_estimate line 61