OAI/MathematicalPhysics/DefocusingNLS/Profile/SlowShiftEquation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The derivative shift throughout the regularized parameter strip

  1. theorem OAI.DefocusingNLS.integral_slowLaplaceKernel_eq line 11
  2. theorem OAI.DefocusingNLS.regularizedSlowSolution_bracket_eq line 25
  3. theorem OAI.DefocusingNLS.integral_slowKernelSpatialDerivative_eq_laplace line 40
  4. theorem OAI.DefocusingNLS.hasDerivAt_regularizedSlowSolution_shift line 53

    Source documentation

    The actual regularized definition satisfies the derivative recurrence on the full parameter strip, including q = 0.

    theorem hasDerivAt_regularizedSlowSolution_shift (q : ℂ) (m : ℕ) (x : ℂ)
    (hq : -1 < q.re) (hx : 0 < x.re) :
    HasDerivAt (regularizedSlowSolution q m)
      (-q * regularizedSlowSolution (q + 1) (m + 1) x) x := by
…

    Mentions: OAI.DefocusingNLS.regularizedSlowSolution

  5. theorem OAI.DefocusingNLS.hasDerivAt_deriv_regularizedSlowSolution line 74