OAI/MathematicalPhysics/DefocusingNLS/Spectrum/SpectralTurningScaledNorm.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The turning-point scaling preserves the shell norm when its frequency weight is scaled as well.

  1. theorem OAI.DefocusingNLS.spectralComplexSqrt_scaled_weight line 11
  2. theorem OAI.DefocusingNLS.spectralShellNorm_scale line 21
  3. theorem OAI.DefocusingNLS.spectralShellNorm_controls_norm line 27
  4. theorem OAI.DefocusingNLS.spectralTurning_scaled_weight line 45
  5. theorem OAI.DefocusingNLS.spectralTurningState_shell_norm line 56