OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralRegularRank.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Regular normalization at the origin forces independence at every positive matching radius.

  1. theorem OAI.DefocusingNLS.spectralRegularField_add line 13
  2. theorem OAI.DefocusingNLS.spectralRegularField_smul line 20
  3. theorem OAI.DefocusingNLS.spectralRegular_zero_at_origin line 26
  4. theorem OAI.DefocusingNLS.spectralRegular_coefficients_at_point line 40
  5. theorem OAI.DefocusingNLS.spectralRegular_at_linearIndependent line 59