OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousCommutatorRows.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Bounded rows of the frequency-localized commutator

Each row of the actual commutator kernel, after a fixed Schwartz frequency cutoff, is a bounded functional on the faithful homogeneous space. This gives pointwise convergence from weak convergence without assuming an unproved compact operator.

  1. def OAI.DefocusingNLS.homogeneousCommutatorRowKernel line 20
  2. def OAI.DefocusingNLS.homogeneousCommutatorRowBound line 25
  3. theorem OAI.DefocusingNLS.homogeneousCommutatorRowKernel_continuous line 30
  4. theorem OAI.DefocusingNLS.homogeneousCommutatorRowBound_nonneg line 35
  5. theorem OAI.DefocusingNLS.homogeneousCommutatorRowKernel_norm_le line 40
  6. theorem OAI.DefocusingNLS.homogeneousCommutatorRow_integrable line 64
  7. def OAI.DefocusingNLS.homogeneousCommutatorRowValue line 73
  8. theorem OAI.DefocusingNLS.homogeneousCommutatorRowValue_norm_le line 77
  9. def OAI.DefocusingNLS.homogeneousCommutatorRow line 109
  10. theorem OAI.DefocusingNLS.homogeneousCommutatorRow_Schwartz line 142
  11. theorem OAI.DefocusingNLS.tendsto_homogeneousCommutatorRow_of_weakNull line 158