OAI/MathematicalPhysics/DefocusingNLS/Profile/SlowSpatialBoundary.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Spatial holomorphy across the nonzero imaginary boundary

  1. theorem OAI.DefocusingNLS.hasDerivAt_integral_regularizedSlowKernel_of_im_ne_zero line 11
  2. theorem OAI.DefocusingNLS.differentiableAt_regularizedSlowSolution_of_im_ne_zero line 53
  3. theorem OAI.DefocusingNLS.differentiableOn_regularizedSlowSolution_slit line 64

    Source documentation

    The original integral, on its natural slit domain, supplies the holomorphic continuation across every nonzero imaginary point.

    theorem differentiableOn_regularizedSlowSolution_slit (q : ℂ) (m : ℕ)
    (hq : -1 < q.re) :
    DifferentiableOn ℂ (regularizedSlowSolution q m) Complex.slitPlane := by
…

    Mentions: OAI.DefocusingNLS.regularizedSlowSolution

  4. theorem OAI.DefocusingNLS.analyticOnNhd_regularizedSlowSolution_slit line 72