OAI/MathematicalPhysics/DefocusingNLS/Profile/SlowEulerDerivative.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Differentiating the Euler representation in the spatial parameter

  1. theorem OAI.DefocusingNLS.norm_slowEulerKernel line 12
  2. theorem OAI.DefocusingNLS.norm_slowEulerKernel_le line 21
  3. theorem OAI.DefocusingNLS.continuousOn_slowEulerKernel line 28
  4. theorem OAI.DefocusingNLS.integrable_slowEulerKernel line 44
  5. theorem OAI.DefocusingNLS.hasDerivAt_slowEulerKernel line 52
  6. theorem OAI.DefocusingNLS.hasDerivAt_integral_slowEulerKernel line 78

    Source documentation

    Differentiation under the Euler integral in its initial half-plane.

    theorem hasDerivAt_integral_slowEulerKernel (q : ℂ) (m : ℕ) (x : ℂ)
    (hq : 0 < q.re) (hx : 0 < x.re) :
    HasDerivAt (fun z : ℂ => ∫ v : ℝ in Set.Ioi 0, slowEulerKernel q m z v)
      (-(∫ v : ℝ in Set.Ioi 0, slowEulerKernel (q + 1) (m + 1) x v)) x := by
…

    Mentions: OAI.DefocusingNLS.slowEulerKernel