OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralFreeCoreBoundary.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The constrained free core conditions give exactly the certified H determinant.

  1. def OAI.DefocusingNLS.spectralFreeCoreBoundary line 12

    Source documentation

    The free core has zero first real channel and a regular harmonic second channel.

    noncomputable def spectralFreeCoreBoundary (ell : ℕ) (r : ℝ) (U : E₄) : Fin 2 → ℂ :=
…
  2. theorem OAI.DefocusingNLS.spectralFreeCoreBoundary_determinant line 15
  3. theorem OAI.DefocusingNLS.spectralFreeCoreBoundary_H_zero_iff line 27
  4. theorem OAI.DefocusingNLS.radialFreeSlowArgument_log line 50
  5. theorem OAI.DefocusingNLS.spectralFreeCoreBoundary_zero_iff_spectralSlowDeterminant line 57