OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralRemoteReductionRestriction.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Restricting the finite reduction to one parameter preserves its exact formula. Individual tail bounds can therefore be used without exchanging the parameter and derivative quantifiers of the uniform estimates.

  1. theorem OAI.DefocusingNLS.spectralRemoteReductionData_restrict line 13
  2. theorem OAI.DefocusingNLS.spectralRemoteReductionFrame_restrict line 24
  3. theorem OAI.DefocusingNLS.spectralRemote_root_reduction_single line 35