OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousCommutatorDecay.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

An integrable output bound for bounded input frequencies

The frequency-localized commutator has a square-integrable row majorant. This is the bounded-frequency counterpart of the R⁻¹ estimate.

  1. theorem OAI.DefocusingNLS.schwartz_polynomial_decay line 18
  2. theorem OAI.DefocusingNLS.homogeneousCommutatorRow_decay line 28