OAI/MathematicalPhysics/DefocusingNLS/Certificates/HighAngularFlux.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DefocusingNLS.highAngular_raw_flux line 10

   Source documentation

   The real flux derivative before completing the kinetic square.

   theorem highAngular_raw_flux (A A' C V E U U' U'' : ℂ)
       (hODE : -A*U''-(A'-C*A)*U'+V*U=E*U) :
       (A'*star U*U'+A*star U'*U'+A*star U*U'').re =
         A.re*Complex.normSq U'+(C*A*star U*U').re+
           (V.re-E.re)*Complex.normSq U := by
   …

2. theorem OAI.DefocusingNLS.highAngular_corrected_flux line 23

   Source documentation

   Adding the correction to the boundary flux produces exactly the bulk potential from the manuscript.

   theorem highAngular_corrected_flux (L N α αL' θ' N' h : ℝ)
       (A' V E U U' U'' : ℂ) (hh : h=1 ∨ h= -1)
       (hODE : -((L : ℂ)+Complex.I*(h*N : ℝ))*U''-
         (A'-Complex.I*(h*θ' : ℝ)*((L : ℂ)+Complex.I*(h*N : ℝ)))*U'+V*U=E*U) :
       (A'*star U*U'+((L : ℂ)+Complex.I*(h*N : ℝ))*star U'*U'+
         ((L : ℂ)+Complex.I*(h*N : ℝ))*star U*U'').re+
         (αL'+θ'*N'/2)*Complex.normSq U+
         (α*L+θ'*N/2)*(2*(star U*U').re) =
       L*Complex.normSq (U'+((α : ℂ)-Complex.I*(h*θ'/2 : ℝ))*U)+
         (V.re-E.re+αL'+θ'*N'/2-L*(α^2+θ'^2/4))*Complex.normSq U := by
   …