HighAngularPathEquation.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Chain rules and the actual gauged equation along a complex contour.

theorem OAI.DefocusingNLS.analyticOnNhd_slowGauge line 11
theorem OAI.DefocusingNLS.analyticOnNhd_gaugedSlowSolution line 17

theorem OAI.DefocusingNLS.analytic_path_derivatives line 23

Source documentation

The first two derivatives along a twice differentiable contour.

theorem analytic_path_derivatives (F : ℂ → ℂ) (γ g : ℝ → ℂ) (s : ℝ)
    (hF : AnalyticAt ℂ F (γ s)) (hγ : ∀ t, HasDerivAt γ (g t) t)
    (g' : ℂ) (hg : HasDerivAt g g' s) :
    deriv (fun t => F (γ t)) s = g s*deriv F (γ s) ∧
      deriv (deriv (fun t => F (γ t))) s =
        g'*deriv F (γ s)+(g s)^2*deriv (deriv F) (γ s) := by
…

theorem OAI.DefocusingNLS.analytic_path_hasDerivAt_deriv line 48

Source documentation

The second chain rule as an actual derivative, for use in the flux derivative.

theorem analytic_path_hasDerivAt_deriv (F : ℂ → ℂ) (γ g : ℝ → ℂ) (s : ℝ)
    (hF : AnalyticAt ℂ F (γ s)) (hγ : ∀ t, HasDerivAt γ (g t) t)
    (g' : ℂ) (hg : HasDerivAt g g' s) :
    HasDerivAt (deriv (fun t => F (γ t)))
      (g'*deriv F (γ s)+(g s)^2*deriv (deriv F) (γ s)) s := by
…

theorem OAI.DefocusingNLS.gaugedSlowSolution_path_equation line 66

Source documentation

The Kummer gauge equation after changing to an arc-length contour.

theorem gaugedSlowSolution_path_equation (q : ℂ) (M : ℕ) (γ g : ℝ → ℂ)
    (s : ℝ) (C : ℂ) (hq : -1 < q.re)
    (hx : 0 ≤ (γ s).re) (hx0 : γ s ≠ 0) (hg0 : g s ≠ 0)
    (hγ : ∀ t, HasDerivAt γ (g t) t) (hg : HasDerivAt g (-C*g s) s) :
    -(γ s/(g s)^2)*deriv (deriv (fun t => gaugedSlowSolution q M (γ t))) s-
      (1/g s+C*(γ s/(g s)^2))*deriv (fun t => gaugedSlowSolution q M (γ t)) s+
      (γ s/4+(M : ℂ)^2/(4*γ s))*gaugedSlowSolution q M (γ s) =
      (((M : ℂ)+1)/2-q)*gaugedSlowSolution q M (γ s) := by
…

Mentions: OAI.DefocusingNLS.gaugedSlowSolution