OAI/MathematicalPhysics/DefocusingNLS/Certificates/MatchingBasisChange.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Separate changes of regular and outgoing bases preserve the matching zeros; invertible holomorphic changes also preserve their multiplicities.

  1. def OAI.DefocusingNLS.matchingBasisChange line 13
  2. theorem OAI.DefocusingNLS.matchingBasisChange_det line 16
  3. theorem OAI.DefocusingNLS.spectralMatchingMatrix_change line 22
  4. theorem OAI.DefocusingNLS.spectralMatchingDeterminant_change line 33
  5. theorem OAI.DefocusingNLS.spectralMatchingDeterminant_change_order line 42