OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralRemoteApproximationSymbol.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform finite expansions and coarse derivative growth imply the order-zero symbol estimates on every escaping logarithmic half-line.

  1. theorem OAI.DefocusingNLS.spectralRemote_approximation_symbol line 13