OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralEventualNoJordan.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The compact no-chain limit gives an eventual exclusion of every first chain.

  1. theorem OAI.DefocusingNLS.spectral_eventually_no_jordan line 11