Rapid Fourier decay of the deterministic cutoff

This module is the deterministic, layer-L2 home of the Schwartz decay used both by the mollified-noise construction and by the R-324 frequency-routing argument. Keeping it above the probability layer prevents the deterministic parametrix from depending on random-noise infrastructure.

@[reducible, inline]

abbrev Anderson4D.EuclideanR4 : Type

The Euclidean-norm copy of the four-dimensional frequency space.

Equations

• Anderson4D.EuclideanR4 = EuclideanSpace ℝ (Fin Anderson4D.dim)

noncomputable def Anderson4D.SmoothCutoff.euclideanSchwartz (ρ : SmoothCutoff) : SchwartzMap EuclideanR4 ℂ

A smooth compactly supported cutoff, transported to Euclidean space and complexified, is a Schwartz function.

Equations

• ρ.euclideanSchwartz = ⋯.toSchwartzMap ⋯

@[simp]

theorem Anderson4D.SmoothCutoff.euclideanSchwartz_apply (ρ : SmoothCutoff) (x : EuclideanR4) : ρ.euclideanSchwartz x = ↑(ρ.toFun ((EuclideanSpace.equiv (Fin dim) ℝ) x))

noncomputable def Anderson4D.SmoothCutoff.euclideanFrequency (ξ : R4) : EuclideanR4

Frequency conversion accounting for mathlib's 2π Fourier normalization.

Equations

• Anderson4D.SmoothCutoff.euclideanFrequency ξ = WithLp.toLp 2 fun (i : Fin Anderson4D.dim) => ξ i / (2 * Real.pi)

@[simp]

theorem Anderson4D.SmoothCutoff.euclideanFrequency_apply (ξ : R4) (i : Fin dim) : (euclideanFrequency ξ).ofLp i = ξ i / (2 * Real.pi)

theorem Anderson4D.SmoothCutoff.fourierR4_eq_euclideanSchwartz_fourier (ρ : SmoothCutoff) (ξ : R4) : fourierR4 ρ.toFun ξ = (FourierTransform.fourier ρ.euclideanSchwartz) (euclideanFrequency ξ)

The project's unnormalized Fourier transform is exactly mathlib's Schwartz Fourier transform sampled at frequency ξ/(2π).

theorem Anderson4D.SmoothCutoff.exists_fourierR4_one_add_norm_bound_nat (ρ : SmoothCutoff) (N : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (ξ : R4), (1 + ‖euclideanFrequency ξ‖) ^ N * ‖fourierR4 ρ.toFun ξ‖ ≤ C

Arbitrary-order rapid Fourier decay in the project's normalization.

theorem Anderson4D.SmoothCutoff.exists_fourierR4_one_add_norm_bound (ρ : SmoothCutoff) : ∃ (C : ℝ), 0 < C ∧ ∀ (ξ : R4), (1 + ‖euclideanFrequency ξ‖) ^ 8 * ‖fourierR4 ρ.toFun ξ‖ ≤ C

The eighth-order specialization used throughout the project.