OAI/MathematicalPhysics/DefocusingNLS/Certificates/BoundaryFormEvaluation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DefocusingNLS.conjugatePolynomial_eval_real line 12
2. theorem OAI.DefocusingNLS.sharpPolynomial_eval_real line 17
3. theorem OAI.DefocusingNLS.hermitianPolynomial_eval line 22
4. theorem OAI.DefocusingNLS.forwardFormEntry_conjugate line 29
5. theorem OAI.DefocusingNLS.reflectedHermitianPolynomial_eval line 38

   Source documentation

   Reflection of the polynomial is exactly the second conjugate channel.

   theorem reflectedHermitianPolynomial_eval (M : ℝ) (s : ℂ)
       (T : Matrix (Fin 2) (Fin 2) (Polynomial ℂ)) (v : ℝ) (i j : Fin 2) :
       (reflectedHermitianPolynomial M s T i j).eval (v : ℂ) =
         forwardFormEntry M s (fun a b => (T a b).eval (v : ℂ)) i j +
         forwardFormEntry M (star s) (fun a b => star ((T a b).eval ((-v : ℝ) : ℂ))) i j := by
   …

   Mentions: OAI.DefocusingNLS.reflectedHermitianPolynomial, OAI.DefocusingNLS.forwardFormEntry

6. theorem OAI.DefocusingNLS.reflectedHermitianPolynomial_eval_diagonal line 48