OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralFreeBoundaryMultiplicity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Passing from the H matching determinant to the physical core boundary preserves analytic vanishing order. The normalization factor is entire and nonzero, including at the symmetry roots.

  1. def OAI.DefocusingNLS.spectralFreeCoreDeterminant line 12
  2. def OAI.DefocusingNLS.spectralFreeCoreFactor line 17
  3. theorem OAI.DefocusingNLS.conjugate_core_factor line 26
  4. theorem OAI.DefocusingNLS.spectralFreeCoreDeterminant_factor line 36
  5. theorem OAI.DefocusingNLS.spectralFreeCoreFactor_analytic_ne_zero line 54
  6. theorem OAI.DefocusingNLS.spectralFreeCoreDeterminant_order line 74