OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralForcingLimit.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Assembly of the actual normalized forcing: the polynomial residual has its free limit and the weighted coefficient error tends to zero.

  1. theorem OAI.DefocusingNLS.circularCoefficientAction_real_smul line 16
  2. theorem OAI.DefocusingNLS.boundedCircularCoefficientAction_factor line 22
  3. theorem OAI.DefocusingNLS.exists_circular_normalized_forcing_limit line 39