OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralTurningOutgoingFlux.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A single oscillatory cutoff retains a positive amount of the outgoing flux for every sufficiently large member of the actual parameter family.

  1. theorem OAI.DefocusingNLS.spectralTurning_eventual_outgoing_flux line 12