SchwartzSobolevLocalization.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Weighted finite Fourier localization

This proves the weighted mixed Fourier bound in the verification of (lin:J-bound). The kernel is a genuine Schwartz function; its positive Bessel-weighted modulus is used only inside the Schur estimate. The later Fourier change of variables must still carry the chosen Fourier normalization.

theorem OAI.DefocusingNLS.localization_bessel_product line 18
theorem OAI.DefocusingNLS.localization_bessel_square line 34

theorem OAI.DefocusingNLS.exists_schwartz_sobolev_localization_bound line 41

Source documentation

Uniform finite-sum estimate for the Sobolev-weighted localization kernel.

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

Mentions: OAI.DefocusingNLS.frequencyLattice