OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousFourierPairing.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Bounded Fourier test functionals on the actual homogeneous space

The inverse weight makes every Y vector an integrable Fourier function. Consequently Schwartz tests act continuously on Y, with their ordinary Lebesgue pairing, rather than an unspecified distributional realization.

  1. theorem OAI.DefocusingNLS.homogeneousFourier_integral_norm_le line 26
  2. theorem OAI.DefocusingNLS.integrable_homogeneousFourier_test line 37
  3. def OAI.DefocusingNLS.homogeneousFourierPairing line 42
  4. theorem OAI.DefocusingNLS.homogeneousFourierPairing_apply line 88
  5. theorem OAI.DefocusingNLS.homogeneousFourierPairing_Schwartz line 91