OAI/MathematicalPhysics/DefocusingNLS/Certificates/RectangleRouche.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Rouché's theorem for the spectral counting rectangle

The specialization of Ahlfors, Complex Analysis, third edition, Chapter 4, §5.2, p. 153, Corollary following Theorem 18 follows from the finite analytic divisor, Cauchy's theorem, and the boundary logarithm of the quotient.

  1. theorem OAI.DefocusingNLS.rectangle_rouche line 14