OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralOutgoingRobinLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A uniformly vanishing local Robin error can be selected along one subsequence, preserving all already established boundary limits.

  1. theorem OAI.DefocusingNLS.spectralOutgoing_robin_limit line 11