OAI/MathematicalPhysics/DefocusingNLS/Profile/NormalizedSlowTail.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

A nonsingular normalization of the slow tail

The only vanishing Pochhammer factor in the relevant half-plane is q. Coefficients of H(q+1,m+1) give the tail divided by this factor without division. The resulting recurrence remains meaningful at q = 0.

  1. def OAI.DefocusingNLS.normalizedSlowB line 16
  2. def OAI.DefocusingNLS.normalizedSlowC line 19
  3. def OAI.DefocusingNLS.normalizedSlowCoefficient line 22
  4. theorem OAI.DefocusingNLS.normalizedSlowB_succ line 26
  5. theorem OAI.DefocusingNLS.normalizedSlowC_succ line 32
  6. theorem OAI.DefocusingNLS.normalizedSlow_recurrence_succ line 37

    Source documentation

    The normalized recurrence holds at the removable parameter q = 0.

    theorem normalizedSlow_recurrence_succ (q : ℂ) (M : ℕ) (s : ℂ) (n : ℕ)
    (hq : -1 < q.re) (hsre : s.re = 0) (hsim : s.im ≠ 0) :
    (q + (n + 1 : ℕ)) * normalizedSlowCoefficient q (M + 1) s (n + 1) =
      -(M : ℂ) * normalizedSlowB q (M + 1) s (n + 2) -
        s * normalizedSlowC q (M + 1) s (n + 1) := by
…

    Mentions: OAI.DefocusingNLS.normalizedSlowCoefficient, OAI.DefocusingNLS.normalizedSlowB, OAI.DefocusingNLS.normalizedSlowC

  7. theorem OAI.DefocusingNLS.normalizedSlow_recurrence line 51
  8. theorem OAI.DefocusingNLS.normalizedSlowB_tendsto_zero line 60
  9. theorem OAI.DefocusingNLS.normalizedSlowC_tendsto_zero line 67