RadianFourierLocalization.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Exact radian Fourier normalization for a localized Fourier polynomial

The torus characters in the manuscript are exp(i n·y/L), while Mathlib's Fourier transform uses exp(-2π i y·ξ). We rescale the transform explicitly.

def OAI.DefocusingNLS.radianFourierIntegral line 20
def OAI.DefocusingNLS.radianFourierKernel line 24
Source documentation
The radian-normalized Fourier transform of a cutoff is still Schwartz.
```
noncomputable def radianFourierKernel (χ : 𝓢(E, ℂ)) : 𝓢(E, ℂ) :=
…
```
theorem OAI.DefocusingNLS.radianFourierKernel_apply line 28

theorem OAI.DefocusingNLS.radianFourier_dilation line 42

Source documentation

Positive dilation in physical space gives exactly the twelve-dimensional Jacobian.

theorem radianFourier_dilation (L : ℝ) (hL : 0 < L) (f : E → ℂ) (ξ : E) :
    radianFourierIntegral (fun y => f (L⁻¹ • y)) ξ =
      (L ^ (12 : ℕ) : ℝ) • radianFourierIntegral f (L • ξ) := by
…

Mentions: OAI.DefocusingNLS.radianFourierIntegral

def OAI.DefocusingNLS.localizedFourierPolynomial line 56
Source documentation
The localized physical Fourier polynomial, before zero extension is needed.
```
noncomputable def localizedFourierPolynomial (L : ℝ) (χ : 𝓢(E, ℂ))
    (S : Finset frequencyLattice) (v : frequencyLattice → ℂ) (y : E) : ℂ :=
…
```
Mentions: OAI.DefocusingNLS.frequencyLattice
theorem OAI.DefocusingNLS.radianFourier_modulated_sum line 60
theorem OAI.DefocusingNLS.localizedFourierPolynomial_transform line 95
Source documentation
The exact finite Fourier cutoff formula, in the manuscript's radian convention.
```
theorem localizedFourierPolynomial_transform (L : ℝ) (hL : 0 < L)
    (χ : 𝓢(E, ℂ)) (S : Finset frequencyLattice) (v : frequencyLattice → ℂ) (ξ : E) :
    radianFourierIntegral (localizedFourierPolynomial L χ S v) ξ =
      (L ^ (12 : ℕ) : ℝ) • ∑ n ∈ S, v n * radianFourierKernel χ (L • ξ - n) := by
…
```
Mentions: OAI.DefocusingNLS.frequencyLattice, OAI.DefocusingNLS.radianFourierIntegral, OAI.DefocusingNLS.localizedFourierPolynomial, OAI.DefocusingNLS.radianFourierKernel