OAI/MathematicalPhysics/DefocusingNLS/Profile/SlowLaplaceRepresentation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The usual integral in the positive parameter half-plane

  1. def OAI.DefocusingNLS.slowLaplaceKernel line 12
  2. theorem OAI.DefocusingNLS.slowLaplaceKernel_eq line 16
  3. theorem OAI.DefocusingNLS.integrable_slowLaplaceKernel line 22
  4. theorem OAI.DefocusingNLS.regularizedSlowSolution_eq_laplace line 37

    Source documentation

    For positive real part of the parameter, the regularized definition agrees with the ordinary Laplace integral.

    theorem regularizedSlowSolution_eq_laplace (q : ℂ) (m : ℕ) (x : ℂ)
    (hq : 0 < q.re) (hx : 0 ≤ x.re) (hx0 : x ≠ 0) :
    regularizedSlowSolution q m x =
      x ^ (-q) * (Complex.Gamma q)⁻¹ *
        ∫ u : ℝ in Set.Ioi 0, slowLaplaceKernel q m x u := by
…

    Mentions: OAI.DefocusingNLS.regularizedSlowSolution, OAI.DefocusingNLS.slowLaplaceKernel