OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralCompactChainLift.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A first-order chain for the actual compact pencil lifts to the constrained weak equations, with both the volume and boundary derivative load retained.

  1. theorem OAI.DefocusingNLS.SpectralPenaltyFamily.limitInverse_complex_load line 11
  2. theorem OAI.DefocusingNLS.SpectralPenaltyFamily.limitPencil_chain_lift line 31