OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousFiniteRankAnalytic.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Holomorphic finite-dimensional obstruction for the linearized step

The Schur determinant is holomorphic on the resolvent of the contracting part. This is the scalar analytic function used to isolate the remaining spectral points of the actual finite-rank decomposition.

  1. theorem OAI.DefocusingNLS.matrix_det_analyticAt line 16

    Distinct definitions of this name: OAI/MathematicalPhysics/DefocusingNLS/Certificates/MatchingMatrixSimpleZero.lean:13 (different declaration text). Qualify references as OAI.DefocusingNLS.matrix_det_analyticAt@path.

  2. theorem OAI.DefocusingNLS.finiteDimensional_det_analyticAt line 35
  3. theorem OAI.DefocusingNLS.operator_resolvent_analyticAt line 49
  4. theorem OAI.DefocusingNLS.finiteRank_determinant_analyticAt line 63