OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralPencilDerivative.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Differentiating the compact pencil preserves exactly the derivative load used in the weak first-chain lift.

  1. theorem OAI.DefocusingNLS.SpectralPenaltyFamily.limitPencil_hasDerivAt line 26
  2. theorem OAI.DefocusingNLS.SpectralPenaltyFamily.limitPencil_derivative_chain_lift line 38