OAI/MathematicalPhysics/DefocusingNLS/Certificates/BoundaryPolynomial.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Polynomial structure of the finite forward matrix

Only the constant coefficient depends on the spectral shift. The leading matrix is computed for every truncation depth, independently of parameters.

  1. def OAI.DefocusingNLS.boundaryLinear line 16
  2. def OAI.DefocusingNLS.boundaryForwardStep line 18
  3. def OAI.DefocusingNLS.boundaryForwardProduct line 22
  4. theorem OAI.DefocusingNLS.boundaryLinear_degree line 27
  5. theorem OAI.DefocusingNLS.boundaryForwardStep_degree line 32
  6. theorem OAI.DefocusingNLS.boundaryForwardProduct_degree line 45
  7. theorem OAI.DefocusingNLS.boundaryLinear_mul_top line 59
  8. theorem OAI.DefocusingNLS.boundaryForwardProduct_top line 65
  9. theorem OAI.DefocusingNLS.boundaryForwardStep_eval line 89
  10. theorem OAI.DefocusingNLS.boundaryForwardProduct_eval line 97

    Source documentation

    Evaluation of the symbolic boundary product gives the actual forward matching matrix on a vertical spectral line.

    theorem boundaryForwardProduct_eval (M : ℝ) (s q : ℂ) (v : ℝ) (K : ℕ)
    (i j : Fin 2) :
    (boundaryForwardProduct M s (fun n => q + n) K i j).eval (v : ℂ) =
      forwardProduct (M : ℂ) s (q + Complex.I * v) K i j := by
…

    Mentions: OAI.DefocusingNLS.boundaryForwardProduct, OAI.DefocusingNLS.forwardProduct