OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousFiniteRankFactor.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Canonical finite-dimensional factor of the actual finite-rank remainder

The factor space is the range of the remainder already constructed from the evolution. No auxiliary factorization or spectral hypothesis is needed.

  1. def OAI.DefocusingNLS.finiteRankRangeMap line 20
  2. theorem OAI.DefocusingNLS.finiteRank_range_factorization line 25
  3. def OAI.DefocusingNLS.finiteRankSchurDet line 30
  4. theorem OAI.DefocusingNLS.finiteRankSchurDet_analyticAt line 35
  5. theorem OAI.DefocusingNLS.finiteRankSchurDet_tendsto_one line 43
  6. theorem OAI.DefocusingNLS.finiteRankSchurDet_spectrum_iff line 48
  7. theorem OAI.DefocusingNLS.finiteRankSchurDet_exists_eigenvector line 58