OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousPhysicalMap.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Bounded linear physical realization of the homogeneous space

Almost-everywhere arithmetic of the Fourier representatives becomes exact arithmetic of the inverse Fourier functions.

  1. theorem OAI.DefocusingNLS.volume_absolutelyContinuous_homogeneousFourierMeasure line 18
  2. theorem OAI.DefocusingNLS.inverseRadianFourier_congr_ae line 28
  3. theorem OAI.DefocusingNLS.inverseRadianFourier_add line 34
  4. theorem OAI.DefocusingNLS.inverseRadianFourier_smul line 39
  5. def OAI.DefocusingNLS.homogeneousPhysicalLinearMap line 45
  6. def OAI.DefocusingNLS.homogeneousPhysicalCLM line 73
  7. theorem OAI.DefocusingNLS.homogeneousPhysicalCLM_apply line 79
  8. theorem OAI.DefocusingNLS.homogeneousPhysicalCLM_Schwartz line 84

    Source documentation

    The physical map agrees with the original Schwartz function on the dense domain.

    theorem homogeneousPhysicalCLM_Schwartz (a k : ℝ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (χ : 𝓢(E, ℂ)) (y : E) :
    homogeneousPhysicalCLM a k ha ha1 hk (homogeneousSchwartzEmbedding a k ha ha1 hk χ) y =
      χ y := by
…

    Mentions: OAI.DefocusingNLS.homogeneousPhysicalCLM, OAI.DefocusingNLS.homogeneousSchwartzEmbedding