Poisson summation for the mollified covariance

This file identifies the absolutely convergent Fourier covariance of the Lebesgue-normalized noise with the spatial periodization of the Euclidean cutoff covariance. It is the deterministic final bridge in blueprint node I-noise.

Euclidean covariance Fourier transform

Rescaling

Characters and periodization on the fundamental cube

theorem Anderson4D.SmoothCutoff.measurable_etaEpsT4 (ρ : SmoothCutoff) (ε : ℝ) : Measurable (ρ.etaEpsT4 ε)

Every positive-scale periodized covariance is Borel measurable.

Fourier coefficient of the periodization

The absolutely convergent torus Fourier series

noncomputable def Anderson4D.SmoothCutoff.covarianceModeCoeff (ρ : SmoothCutoff) (ε : ℝ) (k : Z4) : ℂ

One Fourier coefficient of the Lebesgue-normalized cutoff covariance.

Equations

• ρ.covarianceModeCoeff ε k = ↑Anderson4D.NoiseModel.whiteNoiseFourierScale ^ 2 * ↑(‖ρ.symbol ε k‖ ^ 2)

noncomputable def Anderson4D.SmoothCutoff.complexFourierCovarianceT4 (ρ : SmoothCutoff) (ε : ℝ) (z : T4) : ℂ

The absolutely convergent complex Fourier series of the cutoff covariance. Its values are real, but the complex form is the useful one for frequency routing.

Equations

• ρ.complexFourierCovarianceT4 ε z = ∑' (k : Anderson4D.Z4), ρ.covarianceModeCoeff ε k * Anderson4D.charT4 k z

theorem Anderson4D.SmoothCutoff.summable_norm_covarianceModeCoeff (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) : Summable fun (k : Z4) => ‖ρ.covarianceModeCoeff ε k‖

Fixed-scale boundedness of the periodization

Continuity of the Euclidean periodization

Fourier uniqueness and pointwise upgrade

theorem Anderson4D.SmoothCutoff.complexFourierCovarianceT4_eq_etaEpsT4 (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (z : T4) : ρ.complexFourierCovarianceT4 ε z = ↑(ρ.etaEpsT4 ε z)

theorem Anderson4D.NoiseModel.fourierCovarianceT4_eq_etaEpsT4 (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (z : T4) : fourierCovarianceT4 ρ ε z = ρ.etaEpsT4 ε z

Multidimensional Poisson summation for the mollified covariance, with the exact Lebesgue/probability-Haar normalization whiteNoiseFourierScale² = (2π)⁻⁴.