OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralKernelCoefficientLine.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The free boundary conditions have at most one independent coefficient vector. Nonvanishing is proved for the actual normalized H column.

  1. theorem OAI.DefocusingNLS.matchingColumn_kernel_line line 10
  2. theorem OAI.DefocusingNLS.spectralFreePositivePhysical_core_ne_zero line 35