Deterministic Fourier covariance of the mollified noise

This module records the normalization and absolutely convergent Fourier series underlying the cutoff covariance. Although the normalization is used to construct white noise, every declaration here is deterministic and belongs below the probability layer.

noncomputable def Anderson4D.NoiseModel.whiteNoiseFourierScale : ℝ

Fourier half-density converting the probability-Haar character basis to Lebesgue-normalized white noise on [−π,π]⁴.

Equations

• Anderson4D.NoiseModel.whiteNoiseFourierScale = (2 * Real.pi) ^ (-2)

theorem Anderson4D.NoiseModel.whiteNoiseFourierScale_pos : 0 < whiteNoiseFourierScale

noncomputable def Anderson4D.NoiseModel.fourierCovarianceT4 (ρ : SmoothCutoff) (ε : ℝ) (z : T4) : ℝ

The deterministic Fourier-series covariance associated with the cutoff multiplier, including the Lebesgue white-noise half-density squared.

Equations

• Anderson4D.NoiseModel.fourierCovarianceT4 ρ ε z = (∑' (k : Anderson4D.Z4), ↑Anderson4D.NoiseModel.whiteNoiseFourierScale ^ 2 * ↑(‖ρ.symbol ε k‖ ^ 2) * Anderson4D.charT4 k z).re