OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralTurningOutgoingFamily.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The normalized scalar outgoing solutions can be chosen along an escaping parameter sequence with one bound at any fixed oscillatory cutoff.

  1. theorem OAI.DefocusingNLS.spectralTurning_outgoing_bound_coarse line 12
  2. theorem OAI.DefocusingNLS.spectralTurning_outgoing_family line 29