OAI/MathematicalPhysics/DefocusingNLS/Profile/SlowPositiveRay.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The Euler integral on the positive spatial ray

  1. def OAI.DefocusingNLS.slowEulerKernel line 12
  2. theorem OAI.DefocusingNLS.slowLaplaceKernel_rescale line 16
  3. theorem OAI.DefocusingNLS.integrable_slowEulerKernel_real line 26
  4. theorem OAI.DefocusingNLS.regularizedSlowSolution_eq_euler line 44

    Source documentation

    The substitution used in the manuscript before differentiation and integration by parts.

    theorem regularizedSlowSolution_eq_euler (q : ℂ) (m : ℕ) {x : ℝ}
    (hq : 0 < q.re) (hx : 0 < x) :
    regularizedSlowSolution q m (x : ℂ) = (Complex.Gamma q)⁻¹ *
      ∫ v : ℝ in Set.Ioi 0, slowEulerKernel q m (x : ℂ) v := by
…

    Mentions: OAI.DefocusingNLS.regularizedSlowSolution, OAI.DefocusingNLS.slowEulerKernel