OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralRemoteSymbolInverse.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Inversion of a decaying near-identity change preserves uniform symbol bounds. Consequently an exact block cancellation improves every fixed jet by the same two powers.

  1. theorem OAI.DefocusingNLS.spectralRemote_uniform_inverse line 14
  2. theorem OAI.DefocusingNLS.spectralRemote_uniform_reduction line 46