OAI/MathematicalPhysics/DefocusingNLS/Profile/SlowLaguerreDecay.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Decay and the convergent cone sum for the actual slow solution

  1. theorem OAI.DefocusingNLS.memLp_halfWeighted_shiftedSlowDerivative line 12
  2. theorem OAI.DefocusingNLS.shiftedSlowDerivative_laguerre_tendsto_zero line 20
  3. theorem OAI.DefocusingNLS.slowLaguerreB_tendsto_zero line 26
  4. theorem OAI.DefocusingNLS.slowLaguerreC_tendsto_zero line 33
  5. theorem OAI.DefocusingNLS.hasSum_slowLaguerre_cone_increments line 44

    Source documentation

    The exact infinite cone sum for the actual coefficients. Strict negativity additionally requires a nonzero coefficient beyond the chosen cutoff.

    theorem hasSum_slowLaguerre_cone_increments (σ : ℝ) (ℓ K : ℕ) (q s : ℂ)
    (hσ : -(1 / 32 : ℝ) ≤ σ) (hK : 3 ≤ K)
    (hq : q.re = σ + (ℓ : ℝ) / 2) (hsre : s.re = 0) (hsim : s.im ≠ 0) :
    HasSum (fun n : ℕ => (σ + ((n + K : ℕ) : ℝ) - 5 / 2) *
      Complex.normSq (slowLaguerreCoefficient q (ℓ + 6) s (n + K)))
      (-coneForm ((ℓ : ℝ) + 5) s (slowLaguerreB q (ℓ + 6) s K)
        (slowLaguerreC q (ℓ + 6) s K)) := by
…

    Mentions: OAI.DefocusingNLS.slowLaguerreCoefficient, OAI.DefocusingNLS.coneForm, OAI.DefocusingNLS.slowLaguerreB, OAI.DefocusingNLS.slowLaguerreC