OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/CutoffDiagonalLinearStep.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Normalized linear step data for a profile with a symmetry generator

  1. theorem OAI.DefocusingNLS.cutoffProfile_diagonal_linear_steps line 18