OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralCompactKernelLift.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A kernel vector lifted with its observation already substituted in the weak equation. Keeping this step separate avoids unfolding the coefficient operator during the physical reconstruction.

  1. theorem OAI.DefocusingNLS.SpectralPenaltyFamily.limitPencil_kernel_lift line 12