OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralTurningPairWeight.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A single weight floor works for both turning channels.

  1. theorem OAI.DefocusingNLS.spectralTurning_pair_floor line 10
  2. theorem OAI.DefocusingNLS.spectralTurning_pair_floor_tendsto line 16