OAI/MathematicalPhysics/DefocusingNLS/Certificates/NormalizedTailHolomorphy.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Holomorphy of the normalized tail and its disk-valued ratio

  1. theorem OAI.DefocusingNLS.differentiableAt_slowLaguerreB line 12
  2. theorem OAI.DefocusingNLS.differentiableAt_normalizedSlowB line 25
  3. theorem OAI.DefocusingNLS.differentiableAt_normalizedSlowC line 34
  4. theorem OAI.DefocusingNLS.differentiableAt_normalizedMatchingB line 41
  5. theorem OAI.DefocusingNLS.differentiableAt_normalizedMatchingC line 49
  6. theorem OAI.DefocusingNLS.analyticOnNhd_normalizedMatchingB line 57
  7. theorem OAI.DefocusingNLS.analyticOnNhd_normalizedMatchingC line 64
  8. def OAI.DefocusingNLS.slowTailRatio line 71
  9. theorem OAI.DefocusingNLS.analyticAt_slowTailRatio line 75

    Source documentation

    Holomorphy includes the boundary of the counting half-plane and q=0.

    theorem analyticAt_slowTailRatio (q : ℂ) (ℓ K : ℕ) (s : ℂ)
    (hK : 3 ≤ K) (hq : -(1 / 32 : ℝ) ≤ q.re - (ℓ : ℝ) / 2)
    (hsre : s.re = 0) (hsim : s.im ≠ 0) :
    AnalyticAt ℂ (fun z => slowTailRatio z (ℓ + 6) K s) q := by
…

    Mentions: OAI.DefocusingNLS.slowTailRatio