OAI/MathematicalPhysics/DefocusingNLS/Certificates/LaguerreRapidDecay.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Rapid decay of the actual slow-solution Laguerre coefficients

  1. theorem OAI.DefocusingNLS.laguerreIteratedSlowJet_coefficient_succ line 12
  2. theorem OAI.DefocusingNLS.laguerreIteratedSlowJet_coefficient line 51
  3. theorem OAI.DefocusingNLS.slowLaguerreCoefficient_rapid_decay line 63

    Source documentation

    Every power of the coefficient index times the actual coefficient tends to zero. Each integration by parts is justified by the proved jet bounds.

    theorem slowLaguerreCoefficient_rapid_decay (q : ℂ) (m : ℕ) (s : ℂ)
    (hq : -1 < q.re) (hsre : s.re = 0) (hsim : s.im ≠ 0) (j : ℕ) :
    Tendsto (fun n : ℕ => (n : ℂ) ^ j * slowLaguerreCoefficient q m s n)
      atTop (𝓝 0) := by
…

    Mentions: OAI.DefocusingNLS.slowLaguerreCoefficient