OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralCountingBoundary.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DefocusingNLS.spectralQ line 12
2. def OAI.DefocusingNLS.spectralHomotopyDeterminant line 15
3. theorem OAI.DefocusingNLS.spectralQ_eq_horizontal line 20
4. theorem OAI.DefocusingNLS.spectralHomotopyDeterminant_horizontal line 24
5. theorem OAI.DefocusingNLS.spectralHomotopyDeterminant_left line 33
6. theorem OAI.DefocusingNLS.spectralHomotopyDeterminant_right line 44
7. theorem OAI.DefocusingNLS.exists_spectral_counting_boundary line 58

   Source documentation

   The same height controls every larger rectangle to the right, because points beyond real part eight already lie in the excluded right half-plane.

   theorem exists_spectral_counting_boundary (ell : Fin 4) :
       ∃ V : ℝ, 0 < V ∧ ∀ b Z ρ : ℝ, ∀ z : ℂ,
         |100000000 * b - 33477607| ≤ 2 → |100000000 * Z - 270506819| ≤ 2 →
         0 ≤ ρ → ρ ≤ 1 →
         (z.re = -(1 / 32 : ℝ) ∨ 8 ≤ z.re ∨
           (-(1 / 32 : ℝ) ≤ z.re ∧ V < |z.im|)) →
         spectralHomotopyDeterminant ell b Z ρ z ≠ 0 := by
   …

   Mentions: OAI.DefocusingNLS.spectralHomotopyDeterminant