MixedFourierLocalization.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The mixed Fourier estimate used by torus localization

The localization kernel sends lattice coefficients to a continuous Fourier variable. A finite Schur estimate gives the required ℓ²-to-L² bound; its constants are the uniform periodized L¹ bound and the ordinary L¹ norm of the kernel. No localization bound is assumed.

theorem OAI.DefocusingNLS.mixedFourier_pointwise_bound line 22

Source documentation

Weighted Cauchy--Schwarz for the finite mixed Fourier sum.

theorem mixedFourier_pointwise_bound (S : Finset frequencyLattice)
    (v : frequencyLattice → ℂ)
    (K : EuclideanSpace ℝ (Fin 12) → ℂ)
    (x : EuclideanSpace ℝ (Fin 12)) (C : ℝ)
    (hK : ∑ n ∈ S, ‖K (x - n)‖ ≤ C) :
    ‖∑ n ∈ S, v n * K (x - n)‖ ^ 2 ≤
      C * ∑ n ∈ S, ‖v n‖ ^ 2 * ‖K (x - n)‖ := by
…

Mentions: OAI.DefocusingNLS.frequencyLattice

theorem OAI.DefocusingNLS.mixedFourier_integral_bound line 52

Source documentation

The mixed lattice-to-continuum Fourier kernel is bounded on finite sums. The bound is independent of the finite frequency set.

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

Mentions: OAI.DefocusingNLS.frequencyLattice