OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralRemoteFiniteReduction.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Finite remote block reduction. Every iteration gains two powers, with uniform bounds for all fixed logarithmic derivatives.

  1. abbrev OAI.DefocusingNLS.SpectralRemoteSuperOperator line 13
  2. def OAI.DefocusingNLS.spectralRemoteReductionData line 15
  3. theorem OAI.DefocusingNLS.spectralRemote_finite_reduction line 29