OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousSchwartzCommutator.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Compact top-order commutator for a Schwartz coefficient

The concrete low-frequency part is compact by the kernel row argument. The complementary high-frequency part is uniformly small by the proved R⁻¹ estimate. No Rellich or compact-error hypothesis is assumed.

  1. theorem OAI.DefocusingNLS.commutator_split_energy line 20
  2. theorem OAI.DefocusingNLS.tendsto_homogeneousSchwartzCommutator_fourierL2 line 48
  3. theorem OAI.DefocusingNLS.tendsto_homogeneousSchwartzCommutator_physicalL2 line 104