UniformHorizontalExclusion.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A common upper and lower horizontal counting boundary

theorem OAI.DefocusingNLS.exists_uniform_horizontal_exclusion line 11

Source documentation

Every sufficiently high horizontal line is free of homotopy zeros, uniformly over the compact spectral strip and parameter box.

theorem exists_uniform_horizontal_exclusion (ell : ℕ) (R b₀ b₁ Z₀ Z₁ : ℝ)
    (hZ₀ : 0 < Z₀) :
    ∃ V : ℝ, 0 < V ∧ ∀ σ b Z v ρ : ℝ,
      σ ∈ Set.Icc (-(1 / 32 : ℝ)) R → b ∈ Set.Icc b₀ b₁ → Z ∈ Set.Icc Z₀ Z₁ →
      V < |v| → 0 ≤ ρ → ρ ≤ 1 →
      matchingColumnDeterminant
        (matchingHomotopyColumn (ell + 5) 8 ((1 : ℂ) * Complex.I * Z) ρ
          (horizontalQ ell 1 σ b v))
        (matchingHomotopyColumn (ell + 5) 8 ((-1 : ℂ) * Complex.I * Z) ρ
          (horizontalQ ell (-1) σ b v)) ≠ 0 := by
…

Mentions: OAI.DefocusingNLS.matchingColumnDeterminant, OAI.DefocusingNLS.matchingHomotopyColumn, OAI.DefocusingNLS.horizontalQ