OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralFreeSecondParameterLocal.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.spectralFreeSecond_local_differentiated line 14