OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralRobinColumnDerivative.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Analytic outgoing columns satisfy the derivative of their exact Robin plane.

  1. theorem OAI.DefocusingNLS.spectralJetRobin_column_derivatives line 11
  2. theorem OAI.DefocusingNLS.spectralJetRobin_derivative_plane line 36