OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralHolomorphicSingularLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The holomorphic outgoing columns used in matching have the singular limit constructed from the actual canonical profile.

  1. def OAI.DefocusingNLS.IsCanonicalHolomorphicColumn line 14
  2. theorem OAI.DefocusingNLS.exists_canonical_holomorphic_singular_limit line 26