OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralCircularForcing.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Bounded normalized forcing from the actual profile expansion error.

  1. theorem OAI.DefocusingNLS.exists_circularBounded line 13
  2. theorem OAI.DefocusingNLS.exists_circular_weighted_coefficient_error line 22