OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralOutgoingBounds.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Value and first-derivative bounds for the constructed outgoing spectral columns.

  1. theorem OAI.DefocusingNLS.circular_expansion_bound line 14
  2. theorem OAI.DefocusingNLS.spectralPhysicalJet_bounds line 33