OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousFiniteRankDiscrete.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Finitely many exceptional spectral values outside a larger disk

The finite-dimensional determinant is nonzero near infinity. The identity principle on the exterior disk makes its zeros discrete, and compactness of the ambient spectrum makes every outer portion finite.

  1. theorem OAI.DefocusingNLS.complex_norm_exterior_preconnected line 20
  2. theorem OAI.DefocusingNLS.exterior_mem_resolvent line 48
  3. theorem OAI.DefocusingNLS.finiteRankSchurDet_codiscrete line 54
  4. theorem OAI.DefocusingNLS.finiteRank_spectrum_outer_finite line 69
  5. theorem OAI.DefocusingNLS.finiteRank_exists_resolvent_circle line 89

    Source documentation

    A contracting remainder admits a spectral contour strictly inside the unit circle.

    theorem finiteRank_exists_resolvent_circle (B K : E →L[ℂ] E)
    (hK : FiniteDimensional ℂ (LinearMap.range K.toLinearMap))
    (hB : ‖B‖ < 1) (η : ℝ) (hη : η < 1) :
    ∃ r : ℝ, ‖B‖ < r ∧ η < r ∧ r < 1 ∧
      ∀ z : ℂ, ‖z‖ = r → z ∈ resolventSet ℂ (B + K) := by
…