OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralRadialOpenContinuity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The completed radial representative is continuous throughout the positive-radius domain.

  1. theorem OAI.DefocusingNLS.spectralRadialRepresentative_continuousOn_open line 10