OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousFreeDuality.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact Fourier-test action of the free similarity group

Changing variables moves the dilation onto the test function. This identity holds on the whole homogeneous space by its dense Schwartz realization and provides the distributional generator calculation.

  1. def OAI.DefocusingNLS.homogeneousFreeDualTest line 20
  2. theorem OAI.DefocusingNLS.homogeneousFreeDualTest_apply line 27
  3. theorem OAI.DefocusingNLS.integral_homogeneousFreeFourier_dual line 39
  4. theorem OAI.DefocusingNLS.homogeneousFreeOperator_fourier_duality line 79