OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralRemotePhysicalSymbol.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Physical spectral parameters and odd-power coefficient symbols give the bounded Euler remainder.

  1. theorem OAI.DefocusingNLS.HasUniformLogJetBound.const_family line 11
  2. theorem OAI.DefocusingNLS.spectralRemote_physical_bounded_symbol line 26