OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralRemoteRootReduction.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Finite block reduction for the actual remote leading roots. The Sylvester equations and all uniform derivative bounds are discharged here.

  1. def OAI.DefocusingNLS.spectralRemoteLeadingOperator line 12
  2. theorem OAI.DefocusingNLS.spectralRemote_root_sylvester line 17
  3. theorem OAI.DefocusingNLS.spectralRemote_root_reduction line 33