OAI/MathematicalPhysics/DefocusingNLS/Certificates/HighAngularFluxDerivative.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DefocusingNLS.highAngularFlux line 12
2. theorem OAI.DefocusingNLS.hasDerivAt_complex_normSq line 15
3. theorem OAI.DefocusingNLS.hasDerivAt_highAngularFlux line 26
4. theorem OAI.DefocusingNLS.hasDerivAt_highAngularFlux_completed line 43

   Source documentation

   A local ODE yields the positive-square flux derivative with no integration or unproved endpoint assertion.

   theorem hasDerivAt_highAngularFlux_completed
       (A : ℝ → ℂ) (B : ℝ → ℝ) (U : ℝ → ℂ) (t : ℝ)
       (L N α αL' θ' N' h : ℝ) (A' V E U' U'' : ℂ)
       (hh : h=1 ∨ h= -1)
       (hAval : A t=(L : ℂ)+Complex.I*(h*N : ℝ))
       (hBval : B t=α*L+θ'*N/2)
       (hA : HasDerivAt A A' t)
       (hB : HasDerivAt B (αL'+θ'*N'/2) t)
       (hU : HasDerivAt U U' t) (hU' : HasDerivAt (deriv U) U'' t)
       (hODE : -A t*U''-(A'-Complex.I*(h*θ' : ℝ)*A t)*U'+V*U t=E*U t) :
       HasDerivAt (highAngularFlux A B U)
         (L*Complex.normSq (U'+((α : ℂ)-Complex.I*(h*θ'/2 : ℝ))*U t)+
   …

   Mentions: OAI.DefocusingNLS.highAngularFlux