OAI/MathematicalPhysics/DefocusingNLS/Certificates/NormalizedMatchingColumns.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DefocusingNLS.normalizedSlowC_one line 11
2. theorem OAI.DefocusingNLS.normalizedSlow_initial_column line 20
3. theorem OAI.DefocusingNLS.normalizedSlow_backward_relation line 39
4. theorem OAI.DefocusingNLS.normalizedSlow_backwardProduct line 54

   Source documentation

   The factor q has disappeared from the backward product, with no division in the argument. In particular this formula is valid at q=0.

   theorem normalizedSlow_backwardProduct (q : ℂ) (M K : ℕ) (s : ℂ)
       (hq : -1 < q.re) (hsre : s.re = 0) (hsim : s.im ≠ 0) :
       backwardProduct M s q (K + 1) *ᵥ
         ![normalizedSlowB q (M + 1) s (K + 1), normalizedSlowC q (M + 1) s (K + 1)] =
         (ascPochhammer ℂ K).eval (q + 1) •
           ![regularizedSlowSolution q (M + 1) (-s),
             -deriv (regularizedSlowSolution q (M + 1)) (-s)] := by
   …

   Mentions: OAI.DefocusingNLS.backwardProduct, OAI.DefocusingNLS.normalizedSlowB, OAI.DefocusingNLS.normalizedSlowC, OAI.DefocusingNLS.regularizedSlowSolution

5. theorem OAI.DefocusingNLS.shiftedPochhammer_ne_zero line 76
6. def OAI.DefocusingNLS.normalizedMatchingB line 84
7. def OAI.DefocusingNLS.normalizedMatchingC line 87
8. theorem OAI.DefocusingNLS.normalizedMatching_backwardProduct line 91

   Source documentation

   The fully normalized tail produces precisely the actual boundary jet.

   theorem normalizedMatching_backwardProduct (q : ℂ) (M K : ℕ) (s : ℂ)
       (hK : 0 < K) (hq : -1 < q.re) (hsre : s.re = 0) (hsim : s.im ≠ 0) :
       backwardProduct M s q K *ᵥ
         ![normalizedMatchingB q (M + 1) s K, normalizedMatchingC q (M + 1) s K] =
           ![regularizedSlowSolution q (M + 1) (-s),
             -deriv (regularizedSlowSolution q (M + 1)) (-s)] := by
   …

   Mentions: OAI.DefocusingNLS.backwardProduct, OAI.DefocusingNLS.normalizedMatchingB, OAI.DefocusingNLS.normalizedMatchingC, OAI.DefocusingNLS.regularizedSlowSolution