OAI/MathematicalPhysics/DefocusingNLS/Certificates/RightMatchingExclusion.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DefocusingNLS.normalizedForwardMatrix line 12
2. theorem OAI.DefocusingNLS.normalizedForwardJet_eq_mulVec line 16
3. theorem OAI.DefocusingNLS.matrixCone_normalizedForwardMatrix line 20
4. theorem OAI.DefocusingNLS.ascPochhammer_eval_ne_zero_of_re_pos line 29
5. theorem OAI.DefocusingNLS.matchingHomotopy_right_ne_zero line 43

   Source documentation

   The right boundary may be taken uniformly beyond Re q = ell + 5. This proves absence of homotopy zeros throughout that entire half-plane.

   theorem matchingHomotopy_right_ne_zero (ell K : ℕ) (s q₁ q₂ : ℂ) (ρ : ℝ)
       (hK : 3 ≤ K) (hs : s.re = 0) (hs0 : s.im ≠ 0)
       (hq₁ : (ell : ℝ) + 5 < q₁.re) (hq₂ : (ell : ℝ) + 5 < q₂.re)
       (hρ : 0 ≤ ρ) (hρ1 : ρ ≤ 1) :
       matchingColumnDeterminant
         (matchingHomotopyColumn (ell + 5) K s ρ q₁)
         (matchingHomotopyColumn (ell + 5) K (-s) ρ q₂) ≠ 0 := by
   …

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