OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralTurningFluxLower.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

An explicit flux lower bound for the actual normalized outgoing solution at the positive turning cutoff. The error tends to zero first in the fixed cutoff and then along the escaping parameter sequence.

  1. theorem OAI.DefocusingNLS.spectralTurning_outgoing_flux_lower line 14