OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralPencilLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Compactness and holomorphy also hold for the constrained limiting pencil.

  1. theorem OAI.DefocusingNLS.SpectralPenaltyFamily.limitPencil_compact line 11
  2. theorem OAI.DefocusingNLS.SpectralPenaltyFamily.limitPencil_analyticAt line 37