OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralTailLinear.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The backward circular integral is a bounded complex-linear operator.

  1. theorem OAI.DefocusingNLS.boundedRadialExteriorTail_zero line 11
  2. theorem OAI.DefocusingNLS.boundedRadialExteriorTail_smul line 18
  3. theorem OAI.DefocusingNLS.boundedRadialExteriorTail_add line 35
  4. def OAI.DefocusingNLS.boundedRadialExteriorTailCLM line 53
  5. theorem OAI.DefocusingNLS.circularTail_add line 64
  6. theorem OAI.DefocusingNLS.circularTail_smul line 72
  7. def OAI.DefocusingNLS.circularTailCLM line 80
  8. theorem OAI.DefocusingNLS.circularTailCLM_norm line 91