OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralColumnIdentification.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A column constructed at one fixed sufficient order is the canonical all-orders column on their common exterior ray.

  1. theorem OAI.DefocusingNLS.circular_expansion_matches_allOrders line 13