SchwartzLocalizationKernel.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Schwartz kernels in the mixed Fourier localization estimate

The actual localization kernel is the Fourier transform of a smooth cutoff. Its Bessel-weighted versions remain Schwartz, so the lattice-to-continuum bound applies at both Sobolev orders used in the manuscript.

def OAI.DefocusingNLS.weightedSchwartzKernel line 19

Source documentation

Applying any real Bessel weight preserves the Schwartz localization kernel.

noncomputable def weightedSchwartzKernel (s : ℝ)
    (K : 𝓢(EuclideanSpace ℝ (Fin 12), ℂ)) : 𝓢(EuclideanSpace ℝ (Fin 12), ℂ) :=
…

theorem OAI.DefocusingNLS.weightedSchwartzKernel_apply line 24
theorem OAI.DefocusingNLS.weightedSchwartzKernel_norm line 30

theorem OAI.DefocusingNLS.exists_schwartz_mixedFourier_bound line 37

Source documentation

A concrete Schwartz kernel has a finite mixed L² operator bound.

theorem exists_schwartz_mixedFourier_bound
    (K : 𝓢(EuclideanSpace ℝ (Fin 12), ℂ)) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (S : Finset frequencyLattice) (v : frequencyLattice → ℂ),
      Integrable (fun x => ‖∑ n ∈ S, v n * K (x - n)‖ ^ 2) ∧
        (∫ x, ‖∑ n ∈ S, v n * K (x - n)‖ ^ 2) ≤ C * ∑ n ∈ S, ‖v n‖ ^ 2 := by
…

Mentions: OAI.DefocusingNLS.frequencyLattice

theorem OAI.DefocusingNLS.exists_weightedSchwartz_mixedFourier_bound line 48

Source documentation

The same estimate applies to every real Sobolev weight of the cutoff kernel.

theorem exists_weightedSchwartz_mixedFourier_bound (s : ℝ)
    (K : 𝓢(EuclideanSpace ℝ (Fin 12), ℂ)) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (S : Finset frequencyLattice) (v : frequencyLattice → ℂ),
      Integrable (fun x => ‖∑ n ∈ S, v n * weightedSchwartzKernel s K (x - n)‖ ^ 2) ∧
        (∫ x, ‖∑ n ∈ S, v n * weightedSchwartzKernel s K (x - n)‖ ^ 2) ≤
          C * ∑ n ∈ S, ‖v n‖ ^ 2 :=
…

Mentions: OAI.DefocusingNLS.frequencyLattice, OAI.DefocusingNLS.weightedSchwartzKernel