OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralPencilExclusion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Absence of limiting weak kernels is stable for the actual penalty pencil.

  1. theorem OAI.DefocusingNLS.SpectralPenaltyFamily.compactPencil_eventually_kernel_zero line 11