OAI/MathematicalPhysics/DefocusingNLS/Profile/SlowAdjacentParameter.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Adjacent spatial parameters and the first normalized tail value

  1. theorem OAI.DefocusingNLS.regularizedSlowSolution_adjacent_interior line 11
  2. theorem OAI.DefocusingNLS.regularizedSlowSolution_adjacent line 23
  3. theorem OAI.DefocusingNLS.slowLaguerreCoefficient_zero line 48
  4. theorem OAI.DefocusingNLS.normalizedSlowB_one line 73

    Source documentation

    The first normalized B entry is a boundary value, including when q=0.

    theorem normalizedSlowB_one (q : ℂ) (m : ℕ) (s : ℂ)
    (hq : -1 < q.re) (hsre : s.re = 0) (hsim : s.im ≠ 0) :
    normalizedSlowB q m s 1 = regularizedSlowSolution (q + 1) m (-s) := by
…

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