OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralPenaltyFamily.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Coefficient hypotheses for the singular pressure limit. All fields concern the scalar coefficients; the inverse and its convergence are conclusions.

  1. structure OAI.DefocusingNLS.SpectralPenaltyFamily line 14
  2. def OAI.DefocusingNLS.SpectralPenaltyFamily.inverse line 49
  3. def OAI.DefocusingNLS.SpectralPenaltyFamily.limitInverse line 55
  4. theorem OAI.DefocusingNLS.SpectralPenaltyFamily.inverse_norm line 60
  5. def OAI.DefocusingNLS.SpectralPenaltyFamily.reindex line 66
  6. theorem OAI.DefocusingNLS.SpectralPenaltyFamily.weak_limit_unique line 95