OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralCorrectionParameter.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Differentiating the actual outgoing correction in its weighted Banach space. This retains the source term needed for generalized eigenvectors.

  1. def OAI.DefocusingNLS.circularFieldParameterSlope line 17
  2. theorem OAI.DefocusingNLS.circularFieldParameterSlope_evaluation line 25
  3. theorem OAI.DefocusingNLS.circularFieldOperator_hasParameterDerivAt line 44
  4. theorem OAI.DefocusingNLS.circularResolvedCorrection_parameter_equation line 64
  5. theorem OAI.DefocusingNLS.circularResolvedCorrection_parameter_time_equation line 95
  6. theorem OAI.DefocusingNLS.circularUnweight_hasParameterDerivAt line 127
  7. theorem OAI.DefocusingNLS.circularResolvedCorrection_parameter_unweight_equation line 135