OAI/MathematicalPhysics/DefocusingNLS/Profile/SlowParameterHolomorphy.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Parameter holomorphy up to the imaginary spatial boundary

  1. theorem OAI.DefocusingNLS.continuousOn_slowKernelParameterDerivative line 12
  2. theorem OAI.DefocusingNLS.hasDerivAt_integral_regularizedSlowKernel_parameter line 30
  3. theorem OAI.DefocusingNLS.differentiableAt_regularizedSlowSolution_parameter_closed line 90

    Source documentation

    This includes the purely imaginary spatial arguments used in matching.

    theorem differentiableAt_regularizedSlowSolution_parameter_closed (q : ℂ) (m : ℕ) (x : ℂ)
    (hq : -1 < q.re) (hx : 0 ≤ x.re) (hx0 : x ≠ 0) :
    DifferentiableAt ℂ (fun z : ℂ => regularizedSlowSolution z m x) q := by
…

    Mentions: OAI.DefocusingNLS.regularizedSlowSolution