OAI/MathematicalPhysics/DefocusingNLS/Linear/SchwartzFourierPolynomial.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Finite physical cutoffs are Schwartz

This supplies the dense-domain objects used when extending localization into the manuscript's completed homogeneous Sobolev space.

  1. theorem OAI.DefocusingNLS.spatialFourierCharacter_temperate line 17
  2. def OAI.DefocusingNLS.modulatedSchwartzCutoff line 23
  3. theorem OAI.DefocusingNLS.modulatedSchwartzCutoff_apply line 26
  4. def OAI.DefocusingNLS.localizedSchwartzPolynomial line 31

    Source documentation

    The actual finite cutoff polynomial, bundled in the Schwartz space.

    noncomputable def localizedSchwartzPolynomial (L : ℝ) (hL : 0 < L) (χ : 𝓢(E, ℂ))
    (S : Finset frequencyLattice) (v : frequencyLattice → ℂ) : 𝓢(E, ℂ) :=
…

    Mentions: OAI.DefocusingNLS.frequencyLattice

  5. theorem OAI.DefocusingNLS.localizedSchwartzPolynomial_apply line 37