HomogeneousContourEigenfunction.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Classical eigenfunctions from the actual finite contour generator

The finite-dimensional semigroup generator supplies classical two-channel solutions, and a nonzero contour vector supplies a nonzero physical pair.

def OAI.DefocusingNLS.IsClassicalLinearizedPair line 20
Source documentation
The physical coupled equation, with the actual odd-power coefficients.
```
def IsClassicalLinearizedPair (a b : ℝ) (m : ℕ) (q f g : E → ℂ) (lam : ℂ) : Prop :=
…
```
theorem OAI.DefocusingNLS.homogeneous_physical_pair_nonzero line 31

theorem OAI.DefocusingNLS.homogeneous_contour_generator_classical line 51

Source documentation

Every nonzero eigenvector of the finite contour generator gives a nonzero classical solution of the actual linearized PDE.

theorem homogeneous_contour_generator_classical (a b k : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (m : ℕ) (q : HomogeneousY a k)
    (Q : (HomogeneousY a k × HomogeneousY a k) →L[ℂ]
      (HomogeneousY a k × HomogeneousY a k))
    (hcomm : ∀ t, Commute (homogeneousComplexLinearizedStep a b k ha ha1 hk m q t) Q)
    (hfin : FiniteDimensional ℂ Q.range) (G : Q.range →L[ℂ] Q.range)
    (hG : ∀ t, projectionSemigroupRestriction
      (homogeneousComplexLinearizedStep a b k ha ha1 hk m q) Q hcomm t =
        NormedSpace.exp ((t : ℝ) • G))
    (lam : ℂ) (w : Q.range) (hw : w ≠ 0) (he : G w = lam • w) :
    let P := fun f : HomogeneousY a k =>
…

Mentions: OAI.DefocusingNLS.HomogeneousY, OAI.DefocusingNLS.homogeneousComplexLinearizedStep, OAI.DefocusingNLS.projectionSemigroupRestriction