OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousContourGenerator.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The generator on the actual contour complement

For the manuscript threshold -1/32, a contracting-plus-finite-rank step produces a finite-dimensional generator whose eigenvalues are strictly to the right of that line. The complementary evolution decays exponentially.

  1. def OAI.DefocusingNLS.HasFiniteContourGenerator line 21

    Source documentation

    The exact invariant projection, decaying kernel, and finite generator data.

    def HasFiniteContourGenerator (S : ℝ≥0 → E →L[ℂ] E) : Prop :=
…
  2. theorem OAI.DefocusingNLS.semigroup_contour_generator line 32