OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralFreeParameterLocal.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The zero-profile weighted resolvent provides the actual local holomorphic free H column and its parameter derivative equation.

  1. theorem OAI.DefocusingNLS.spectralFreeFirst_local_differentiated line 14