OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralComplexLinear.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The complex linear inverse of a real coercive form compatible with multiplication by i.

  1. theorem OAI.DefocusingNLS.spectralCompatibleInner_I line 9
  2. theorem OAI.DefocusingNLS.spectralInner_I line 25
  3. def OAI.DefocusingNLS.spectralComplexLinearOfI line 30
  4. def OAI.DefocusingNLS.spectralHermitianInverse line 51