OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralCoerciveRestriction.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Restricting a coercive form and its input to a complete closed subspace.

  1. def OAI.DefocusingNLS.spectralRestrictedForm line 12
  2. theorem OAI.DefocusingNLS.spectralRestrictedForm_coercive line 15
  3. def OAI.DefocusingNLS.spectralRestrictedInput line 22
  4. def OAI.DefocusingNLS.spectralRestrictedInverse line 28
  5. theorem OAI.DefocusingNLS.spectralRestrictedInverse_mem line 33
  6. theorem OAI.DefocusingNLS.spectralRestrictedInverse_equation line 39
  7. theorem OAI.DefocusingNLS.spectralRestrictedInverse_unique line 45
  8. theorem OAI.DefocusingNLS.spectralRestrictedInverse_norm line 52