OAI/MathematicalPhysics/DefocusingNLS/Certificates/ZeroTailParameterContinuity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Joint parameter continuity of the finite zero-tail determinant

At tail parameter zero the matching column is the second column of the finite backward matrix product. Its continuity therefore holds for all parameters, without any integral-kernel continuity or nonvanishing hypothesis.

  1. theorem OAI.DefocusingNLS.continuous_backwardMatrix_entry line 18
  2. theorem OAI.DefocusingNLS.continuous_backwardProduct_entry line 30
  3. theorem OAI.DefocusingNLS.matchingHomotopyColumn_zero_entry line 41
  4. abbrev OAI.DefocusingNLS.ZeroTailParameters line 47

    Source documentation

    Coordinates are the real shift, real coupling, and complex spectral value.

    abbrev ZeroTailParameters := ℝ × ℝ × ℂ
  5. theorem OAI.DefocusingNLS.continuous_zeroTail_spectralColumn line 49
  6. theorem OAI.DefocusingNLS.continuous_zeroTail_spectralDeterminant line 60