OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousCommutatorPotential.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Compact commutator for every actual Y coefficient

The coefficient approximation is in the faithful physical algebra norm. In particular the theorem applies to the coefficients of the constructed profile, without assuming extra rapid decay for that profile.

  1. theorem OAI.DefocusingNLS.tendsto_homogeneousTopCommutator line 17