OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingPhysicalLocalization.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual torus cutoff in Euclidean coordinates

This identifies the Euclidean Fourier-series localization with χ(y/L)v(y) for the previously constructed continuous function on the expanding torus.

  1. def OAI.DefocusingNLS.euclideanToTorus line 20
  2. theorem OAI.DefocusingNLS.torusCharacter_euclidean line 23
  3. def OAI.DefocusingNLS.expandingPhysicalLocalization line 46

    Source documentation

    χ(y/L) times the genuine continuous expanding-torus function.

    noncomputable def expandingPhysicalLocalization (a k L : ℝ) (χ : 𝓢(E, ℂ))
    (f : FourierL2) (y : E) : ℂ :=
…

    Mentions: OAI.DefocusingNLS.FourierL2

  4. theorem OAI.DefocusingNLS.expandingPhysicalLocalization_eq_series line 50
  5. theorem OAI.DefocusingNLS.integrable_expandingPhysicalLocalization line 60