OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralPencilFlux.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Classical local flux and derivative for every limiting compact-pencil kernel vector.

  1. theorem OAI.DefocusingNLS.SpectralPenaltyFamily.limitPencil_classical_second line 11