OAI/MathematicalPhysics/DefocusingNLS/Certificates/MatchingHomotopy.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DefocusingNLS.analyticAt_backwardMatrix_entry line 11
2. theorem OAI.DefocusingNLS.analyticAt_backwardProduct_entry line 23
3. def OAI.DefocusingNLS.matchingHomotopyColumn line 34
4. theorem OAI.DefocusingNLS.analyticAt_matchingHomotopyColumn line 37
5. theorem OAI.DefocusingNLS.matchingHomotopyColumn_zero line 50
6. theorem OAI.DefocusingNLS.matchingHomotopyColumn_one line 54
7. theorem OAI.DefocusingNLS.matchingHomotopyColumn_one_ne_zero line 62
8. theorem OAI.DefocusingNLS.analyticAt_matchingTailScalar line 76

   Source documentation

   The scalar identifying the endpoint with the actual column is holomorphic and nonzero throughout the counting half-plane, including q=0.

   theorem analyticAt_matchingTailScalar (ℓ K : ℕ) (s q : ℂ)
       (hK : 3 ≤ K) (hq : -(1 / 32 : ℝ) ≤ q.re - (ℓ : ℝ) / 2)
       (hsre : s.re = 0) (hsim : s.im ≠ 0) :
       AnalyticAt ℂ (fun z => (normalizedMatchingC z (ℓ + 6) s K)⁻¹) q ∧
         (normalizedMatchingC q (ℓ + 6) s K)⁻¹ ≠ 0 := by
   …

   Mentions: OAI.DefocusingNLS.normalizedMatchingC

9. def OAI.DefocusingNLS.matchingColumnDeterminant line 87
10. theorem OAI.DefocusingNLS.matchingColumnDeterminant_smul line 89
11. theorem OAI.DefocusingNLS.matchingHomotopy_endpoint_determinant line 94