OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousContourDecomposition.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite-dimensional complement of the decaying contour space

The decomposition is derived from a contraction plus a finite-rank operator. Every bounded operator commuting with the time step preserves both pieces.

  1. theorem OAI.DefocusingNLS.finiteRange_isCompactOperator line 23
  2. theorem OAI.DefocusingNLS.finiteRank_contour_decomposition line 31