OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralRadialCoreTrace.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The vanishing-volume core condition also gives zero trace at its positive boundary.

  1. theorem OAI.DefocusingNLS.spectralRadialVolume_absolutelyContinuous line 11
  2. theorem OAI.DefocusingNLS.spectralRadialCore_point_zero line 20