OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralHomotopyHolomorphy.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DefocusingNLS.analyticAt_spectralQ line 11
2. theorem OAI.DefocusingNLS.spectralQ_re line 16
3. theorem OAI.DefocusingNLS.analyticAt_spectralHomotopyColumn line 19
4. theorem OAI.DefocusingNLS.analyticAt_spectralHomotopyDeterminant line 33

   Source documentation

   Every member of the tail homotopy is holomorphic on a neighborhood of the closed counting half-plane.

   theorem analyticAt_spectralHomotopyDeterminant (ell : ℕ) (b Z ρ : ℝ) (z : ℂ)
       (hZ : Z ≠ 0) (hz : -(1 / 32 : ℝ) ≤ z.re) :
       AnalyticAt ℂ (spectralHomotopyDeterminant ell b Z ρ) z := by
   …

   Mentions: OAI.DefocusingNLS.spectralHomotopyDeterminant