OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousJordanChannels.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The exact PDE source associated with a finite Jordan chain

The relation G w = λ w + v gives the physical source v in both circular channels. All contour vectors are in the actual generator domain.

  1. def OAI.DefocusingNLS.IsClassicalLinearizedSourcePair line 19

    Source documentation

    The coupled eigenvalue equation with an explicitly represented source.

    def IsClassicalLinearizedSourcePair (a b : ℝ) (m : ℕ)
    (q f g F G : E → ℂ) (lam : ℂ) : Prop :=
…
  2. theorem OAI.DefocusingNLS.homogeneous_contour_jordan_channels line 31