OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousCompactObservation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Compact local observation of the faithful homogeneous space

Restricting the actual inverse Fourier function to a compact spatial set is a compact linear operator. Norm-continuity of the point evaluations provides the equicontinuity required by Arzelà–Ascoli.

  1. def OAI.DefocusingNLS.homogeneousLocalObservation line 21
  2. theorem OAI.DefocusingNLS.homogeneousLocalObservation_apply line 46
  3. theorem OAI.DefocusingNLS.isCompact_homogeneousLocalObservation_unitBall line 52
  4. theorem OAI.DefocusingNLS.isCompactOperator_homogeneousLocalObservation line 103