OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousLocalL2.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Compact local L² observation

The measure is ordinary Lebesgue measure on the closed Euclidean ball. The observation agrees almost everywhere with the actual physical Fourier realization and is compact by the already proved uniform local observation.

  1. def OAI.DefocusingNLS.homogeneousBallMeasure line 19
  2. instance OAI.DefocusingNLS.homogeneousBallMeasure_finite line 23
  3. def OAI.DefocusingNLS.homogeneousLocalL2Observation line 30
  4. theorem OAI.DefocusingNLS.homogeneousLocalL2Observation_ae line 36
  5. theorem OAI.DefocusingNLS.isCompactOperator_homogeneousLocalL2Observation line 42