OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralHomotopyCount.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DefocusingNLS.exists_spectral_rectangle_homotopy_count line 13

   Source documentation

   The certified zero-free boundary and joint continuity transport the actual analytic zero count from the zero tail to the outgoing endpoint. The only conditional input is the published rectangle case of Rouché's theorem.

   theorem exists_spectral_rectangle_homotopy_count (hR : RectangleRouche) (ell : Fin 4) :
       ∃ V : ℝ, 0 < V ∧ ∀ b Z : ℝ,
         |100000000 * b - 33477607| ≤ 2 → |100000000 * Z - 270506819| ≤ 2 →
         rectangleZeroCount V (spectralHomotopyDeterminant ell b Z 0) =
           rectangleZeroCount V (spectralHomotopyDeterminant ell b Z 1) := by
   …

   Mentions: OAI.DefocusingNLS.RectangleRouche, OAI.DefocusingNLS.rectangleZeroCount, OAI.DefocusingNLS.spectralHomotopyDeterminant