OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousFiniteRankLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The finite-dimensional obstruction tends to one at infinity

The same exact determinant that detects the exceptional spectrum is not identically zero: the ambient resolvent tends to zero in operator norm.

  1. theorem OAI.DefocusingNLS.finiteRank_determinant_tendsto_one line 20
  2. theorem OAI.DefocusingNLS.finiteRank_determinant_eventually_ne_zero line 40