OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralHolomorphicHRobinLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual Robin matrix converges to the matrix of the explicit free H basis.

  1. theorem OAI.DefocusingNLS.exists_canonical_holomorphic_H_robin_limit_with_det line 13
  2. theorem OAI.DefocusingNLS.exists_canonical_holomorphic_H_robin_limit line 63