RectangleRoucheInput.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Rouché's theorem on the spectral counting rectangle

The rectangle specialization of Rouché's theorem is formulated as a proposition. See L. V. Ahlfors, Complex Analysis, third edition, McGraw-Hill, 1979, Chapter 4, §5.2, p. 153, Corollary following Theorem 18. The zero count uses analytic vanishing orders, including multiplicity.

def OAI.DefocusingNLS.countingRectangle line 20
def OAI.DefocusingNLS.closedCountingRectangle line 23
def OAI.DefocusingNLS.countingRectangleBoundary line 26
def OAI.DefocusingNLS.rectangleZeroCount line 29
def OAI.DefocusingNLS.RectangleRouche line 34
Source documentation
Ahlfors's Rouché corollary, specialized to the one family of rectangles used for the spectral count. No spectral conclusion is included in this input.
```
def RectangleRouche : Prop :=
…
```
theorem OAI.DefocusingNLS.isOpen_countingRectangle line 41
theorem OAI.DefocusingNLS.isCompact_closedCountingRectangle line 47
theorem OAI.DefocusingNLS.isCompact_countingRectangleBoundary line 54
theorem OAI.DefocusingNLS.mem_countingRectangleBoundary_iff line 58