Infinite Fourier series for the mollified noise

This file supplies the analytic infinite-series layer of blueprint node I-noise. The cutoff is first transported from the project's sup-norm model of ℝ⁴ to Euclidean space. Compact support and smoothness make it a Schwartz function, so its Fourier multiplier has rapid decay. The probabilistic statements below then isolate the exact summability input needed to pass from finite Fourier sums to the totalized tsum.

theorem Anderson4D.charT4_sub_point (k : Z4) (x y : T4) : charT4 k (x - y) = charT4 k x * charT4 (-k) y

Spatial subtraction law for a torus Fourier character.

Absolute convergence of the random Fourier series

theorem Anderson4D.NoiseModel.measurable_xiEps_joint (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) : Measurable fun (p : M.Ω × T4) => M.xiEps ρ ε p.1 p.2

Joint measurability of the totalized mollified Fourier series in the noise sample and the torus point.

theorem Anderson4D.NoiseModel.measurable_xiEps (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (x : T4) : Measurable fun (ω : M.Ω) => M.xiEps ρ ε ω x

The totalized infinite mollified Fourier series is measurable in the noise sample for every fixed spatial point. No summability hypothesis is needed: measurability of tsum includes its junk value off the summable branch.

theorem Anderson4D.NoiseModel.integral_norm_g_sq (M : NoiseModel) (k : Z4) : ∫ (ω : M.Ω), ‖M.g k ω‖ ^ 2 = 1

The covariance normalization gives unit L² norm for every complex Fourier coefficient.

theorem Anderson4D.NoiseModel.integral_norm_g_le_one (M : NoiseModel) (k : Z4) : ∫ (ω : M.Ω), ‖M.g k ω‖ ≤ 1

Every normalized Fourier coefficient has first absolute moment at most one.

theorem Anderson4D.NoiseModel.integral_norm_g_mul_g_le_one (M : NoiseModel) (k l : Z4) : ∫ (ω : M.Ω), ‖M.g k ω * M.g l ω‖ ≤ 1

Cauchy--Schwarz and the unit second moments bound the first absolute moment of any coefficient product.

noncomputable def Anderson4D.NoiseModel.mollifiedRandomCoeff (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (k : Z4) (ω : M.Ω) : ℂ

The random coefficient of the mollified Fourier series before evaluation at a torus character.

Equations

• M.mollifiedRandomCoeff ρ ε k ω = ρ.symbol ε k * M.g k ω

theorem Anderson4D.NoiseModel.measurable_mollifiedRandomCoeff (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (k : Z4) : Measurable (M.mollifiedRandomCoeff ρ ε k)

theorem Anderson4D.NoiseModel.integrable_mollifiedRandomCoeff (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (k : Z4) : MeasureTheory.Integrable (M.mollifiedRandomCoeff ρ ε k) MeasureTheory.volume

theorem Anderson4D.NoiseModel.integral_norm_mollifiedRandomCoeff_le (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (k : Z4) : ∫ (ω : M.Ω), ‖M.mollifiedRandomCoeff ρ ε k ω‖ ≤ ‖ρ.symbol ε k‖

The L¹ norm of one random coefficient is bounded by the deterministic symbol norm.

theorem Anderson4D.NoiseModel.eLpNorm_one_mollifiedRandomCoeff_le (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (k : Z4) : MeasureTheory.eLpNorm (M.mollifiedRandomCoeff ρ ε k) 1 MeasureTheory.volume ≤ ENNReal.ofReal ‖ρ.symbol ε k‖

The L¹ seminorm of one random coefficient is bounded by the deterministic symbol norm, in ℝ≥0∞ form.

theorem Anderson4D.NoiseModel.ae_summable_norm_mollifiedRandomCoeff (M : NoiseModel) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) : ∀ᵐ (ω : M.Ω), Summable fun (k : Z4) => ‖M.mollifiedRandomCoeff ρ ε k ω‖

At positive scale, the random mollified coefficients are absolutely summable almost surely.

noncomputable def Anderson4D.NoiseModel.weightedMollifiedRandomCoeff (M : NoiseModel) (r : ℕ) (ρ : SmoothCutoff) (ε : ℝ) (k : Z4) (ω : M.Ω) : ℂ

Polynomially weighted random mollified coefficient.

Equations

• M.weightedMollifiedRandomCoeff r ρ ε k ω = ↑(Anderson4D.latticePolynomialWeight r k) * M.mollifiedRandomCoeff ρ ε k ω

theorem Anderson4D.NoiseModel.measurable_weightedMollifiedRandomCoeff (M : NoiseModel) (r : ℕ) (ρ : SmoothCutoff) (ε : ℝ) (k : Z4) : Measurable (M.weightedMollifiedRandomCoeff r ρ ε k)

theorem Anderson4D.NoiseModel.integrable_weightedMollifiedRandomCoeff (M : NoiseModel) (r : ℕ) (ρ : SmoothCutoff) (ε : ℝ) (k : Z4) : MeasureTheory.Integrable (M.weightedMollifiedRandomCoeff r ρ ε k) MeasureTheory.volume

theorem Anderson4D.NoiseModel.integral_norm_weightedMollifiedRandomCoeff_le (M : NoiseModel) (r : ℕ) (ρ : SmoothCutoff) (ε : ℝ) (k : Z4) : ∫ (ω : M.Ω), ‖M.weightedMollifiedRandomCoeff r ρ ε k ω‖ ≤ latticePolynomialWeight r k * ‖ρ.symbol ε k‖

theorem Anderson4D.NoiseModel.eLpNorm_one_weightedMollifiedRandomCoeff_le (M : NoiseModel) (r : ℕ) (ρ : SmoothCutoff) (ε : ℝ) (k : Z4) : MeasureTheory.eLpNorm (M.weightedMollifiedRandomCoeff r ρ ε k) 1 MeasureTheory.volume ≤ ENNReal.ofReal (latticePolynomialWeight r k * ‖ρ.symbol ε k‖)

theorem Anderson4D.NoiseModel.ae_summable_norm_weightedMollifiedRandomCoeff (M : NoiseModel) (r : ℕ) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) : ∀ᵐ (ω : M.Ω), Summable fun (k : Z4) => ‖M.weightedMollifiedRandomCoeff r ρ ε k ω‖

Every polynomial weight is almost surely summable at positive scale.

theorem Anderson4D.NoiseModel.ae_forall_nat_summable_norm_weightedMollifiedRandomCoeff (M : NoiseModel) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) : ∀ᵐ (ω : M.Ω), ∀ (r : ℕ), Summable fun (k : Z4) => ‖M.weightedMollifiedRandomCoeff r ρ ε k ω‖

One event of probability one works simultaneously for every polynomial degree.

theorem Anderson4D.NoiseModel.ae_forall_nat_scale_forall_nat_weight (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) : ∀ᵐ (ω : M.Ω), ∀ (n r : ℕ), Summable fun (k : Z4) => ‖M.weightedMollifiedRandomCoeff r ρ (ε n) k ω‖

A single probability-one event works for every polynomial degree and every member of an arbitrary countable family of positive scales (in particular for any prescribed sequence εₙ ↓ 0).

theorem Anderson4D.NoiseModel.ae_forall_summable_norm_mollified_fourier (M : NoiseModel) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) : ∀ᵐ (ω : M.Ω), ∀ (x : T4), Summable fun (k : Z4) => ‖ρ.symbol ε k * M.g k ω * charT4 k x‖

A single probability-one event gives absolute convergence at every spatial point, since torus characters have norm one.

theorem Anderson4D.NoiseModel.ae_forall_summable_mollified_fourier (M : NoiseModel) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) : ∀ᵐ (ω : M.Ω), ∀ (x : T4), Summable fun (k : Z4) => ρ.symbol ε k * M.g k ω * charT4 k x

Hence the complex random Fourier series converges at every spatial point on the same probability-one event.

theorem Anderson4D.NoiseModel.conj_tsum_mollified_fourier_eq (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (ω : M.Ω) (x : T4) : (starRingEnd ℂ) (∑' (k : Z4), ρ.symbol ε k * M.g k ω * charT4 k x) = ∑' (k : Z4), ρ.symbol ε k * M.g k ω * charT4 k x

The infinite complex Fourier sum is pointwise real. This identity uses the exact k ↦ -k reality constraints and is valid independently of summability because both conjugation and reindexing preserve the junk-totalized tsum.

theorem Anderson4D.NoiseModel.tsum_mollified_fourier_im_eq_zero (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (ω : M.Ω) (x : T4) : (∑' (k : Z4), ρ.symbol ε k * M.g k ω * charT4 k x).im = 0

The imaginary part of the infinite Fourier series vanishes.

theorem Anderson4D.NoiseModel.continuous_xiEps_of_summable (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (ω : M.Ω) (hω : Summable fun (k : Z4) => ‖M.mollifiedRandomCoeff ρ ε k ω‖) : Continuous (M.xiEps ρ ε ω)

Absolute summability of the random coefficients gives uniform convergence and hence continuity of the mollified field.

theorem Anderson4D.NoiseModel.ae_continuous_xiEps (M : NoiseModel) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) : ∀ᵐ (ω : M.Ω), Continuous (M.xiEps ρ ε ω)

For every positive scale, the totalized mollified field is continuous almost surely.

Infinite covariance before the Poisson identification

noncomputable def Anderson4D.NoiseModel.xiEpsC (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (ω : M.Ω) (x : T4) : ℂ

Complex version of the mollified field. Its imaginary part is zero by tsum_mollified_fourier_im_eq_zero.

Equations

• M.xiEpsC ρ ε ω x = ∑' (k : Anderson4D.Z4), Anderson4D.NoiseModel.mollifiedModeCoeff ρ ε x k * M.g k ω

theorem Anderson4D.NoiseModel.xiEpsC_eq_scale_mul_tsum (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (ω : M.Ω) (x : T4) : M.xiEpsC ρ ε ω x = ↑whiteNoiseFourierScale * ∑' (k : Z4), ρ.symbol ε k * M.g k ω * charT4 k x

The complex field is the raw Fourier series multiplied by the Lebesgue white-noise half-density (2π)⁻².

@[simp]

theorem Anderson4D.NoiseModel.xiEpsC_re (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (ω : M.Ω) (x : T4) : (M.xiEpsC ρ ε ω x).re = M.xiEps ρ ε ω x

@[simp]

theorem Anderson4D.NoiseModel.xiEpsC_im (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (ω : M.Ω) (x : T4) : (M.xiEpsC ρ ε ω x).im = 0

noncomputable def Anderson4D.NoiseModel.mollifiedPairTerm (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (x y : T4) (p : Z4 × Z4) (ω : M.Ω) : ℂ

One term in the double Fourier expansion of the two-field covariance.

Equations

• M.mollifiedPairTerm ρ ε x y p ω = Anderson4D.NoiseModel.mollifiedModeCoeff ρ ε x p.1 * M.g p.1 ω * (Anderson4D.NoiseModel.mollifiedModeCoeff ρ ε y p.2 * M.g p.2 ω)

theorem Anderson4D.NoiseModel.integrable_mollifiedPairTerm (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (x y : T4) (p : Z4 × Z4) : MeasureTheory.Integrable (M.mollifiedPairTerm ρ ε x y p) MeasureTheory.volume

theorem Anderson4D.NoiseModel.integral_mollifiedPairTerm (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (x y : T4) (p : Z4 × Z4) : ∫ (ω : M.Ω), M.mollifiedPairTerm ρ ε x y p ω = mollifiedModeCoeff ρ ε x p.1 * mollifiedModeCoeff ρ ε y p.2 * if p.1 = -p.2 then 1 else 0

theorem Anderson4D.NoiseModel.integral_norm_mollifiedPairTerm_le (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (x y : T4) (p : Z4 × Z4) : ∫ (ω : M.Ω), ‖M.mollifiedPairTerm ρ ε x y p ω‖ ≤ ‖mollifiedModeCoeff ρ ε x p.1‖ * ‖mollifiedModeCoeff ρ ε y p.2‖

theorem Anderson4D.NoiseModel.ae_xiEpsC_mul_eq_tsum_pair (M : NoiseModel) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (x y : T4) : (fun (ω : M.Ω) => M.xiEpsC ρ ε ω x * M.xiEpsC ρ ε ω y) =ᵐ[MeasureTheory.volume] fun (ω : M.Ω) => ∑' (p : Z4 × Z4), M.mollifiedPairTerm ρ ε x y p ω

The product of the two infinite Fourier sums is the double tsum almost surely.

theorem Anderson4D.NoiseModel.integral_xiEpsC_mul_eq_tsum_pair (M : NoiseModel) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (x y : T4) : ∫ (ω : M.Ω), M.xiEpsC ρ ε ω x * M.xiEpsC ρ ε ω y = ∑' (p : Z4 × Z4), mollifiedModeCoeff ρ ε x p.1 * mollifiedModeCoeff ρ ε y p.2 * if p.1 = -p.2 then 1 else 0

Exact covariance of the two infinite complex Fourier sums, before collapsing the Kronecker factor.

theorem Anderson4D.NoiseModel.tsum_pair_covariance_collapse (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (x y : T4) : (∑' (p : Z4 × Z4), mollifiedModeCoeff ρ ε x p.1 * mollifiedModeCoeff ρ ε y p.2 * if p.1 = -p.2 then 1 else 0) = ∑' (k : Z4), mollifiedModeCoeff ρ ε x k * mollifiedModeCoeff ρ ε y (-k)

The Kronecker covariance collapses the double Fourier sum to the paired single sum.

theorem Anderson4D.NoiseModel.integral_xiEps_mul_eq_re_tsum (M : NoiseModel) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (x y : T4) : ∫ (ω : M.Ω), M.xiEps ρ ε ω x * M.xiEps ρ ε ω y = (∑' (k : Z4), mollifiedModeCoeff ρ ε x k * mollifiedModeCoeff ρ ε y (-k)).re

Exact covariance of the actual real-valued totalized field, in single Fourier-series form.

theorem Anderson4D.NoiseModel.paired_mollified_mode_eq_norm_sq (ρ : SmoothCutoff) (ε : ℝ) (k : Z4) (x y : T4) : mollifiedModeCoeff ρ ε x k * mollifiedModeCoeff ρ ε y (-k) = ↑whiteNoiseFourierScale ^ 2 * ↑(‖ρ.symbol ε k‖ ^ 2) * charT4 k (x - y)

Algebraic normalization of one paired covariance mode.

theorem Anderson4D.NoiseModel.integral_xiEps_mul_eq_fourierCovarianceT4 (M : NoiseModel) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (x y : T4) : ∫ (ω : M.Ω), M.xiEps ρ ε ω x * M.xiEps ρ ε ω y = fourierCovarianceT4 ρ ε (x - y)

Exact covariance of the mollified field in probability-Haar Fourier form. The remaining spatial-side identification is a separate multidimensional Poisson-summation theorem. The coefficient whiteNoiseFourierScale ^ 2 = (2π)⁻⁴ is exactly the reciprocal-volume factor needed for the intended identity fourierCovarianceT4 ρ ε = ρ.etaEpsT4 ε.