OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralFreeSlowBoundary.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The physical free column and the H/H' column used by the certified determinant.

  1. theorem OAI.DefocusingNLS.spectralFreeAngularPhysical_eq_H_jet line 10
  2. theorem OAI.DefocusingNLS.spectralFreeAngularPhysical_eq_boundaryColumn line 35