Finite-dimensional Gaussianity of the mollified noise

The mollified field is an infinite Fourier series. This file proves that every finite real linear combination of its spatial values has a centered Gaussian law. We enumerate the lattice, use the NoiseModel Gaussian interface for each finite prefix, and pass to the limit in L².

noncomputable def Anderson4D.z4Enumeration : ℕ ≃ Z4

A fixed enumeration of the four-dimensional frequency lattice.

Equations

• Anderson4D.z4Enumeration = Classical.choice Anderson4D.z4Enumeration._proof_1

noncomputable def Anderson4D.noiseModePrefix (N : ℕ) : Finset Z4

The first N modes in the fixed lattice enumeration.

Equations

• Anderson4D.noiseModePrefix N = Finset.map Anderson4D.z4Enumeration.toEmbedding (Finset.range N)

noncomputable def Anderson4D.NoiseModel.xiEpsLinearModeCoeff {n : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (x : Fin n → T4) (a : Fin n → ℝ) (k : Z4) : ℂ

Deterministic Fourier coefficient of a finite real spatial linear combination of the mollified field.

Equations

• Anderson4D.NoiseModel.xiEpsLinearModeCoeff ρ ε x a k = ∑ i : Fin n, ↑(a i) * Anderson4D.NoiseModel.mollifiedModeCoeff ρ ε (x i) k

noncomputable def Anderson4D.NoiseModel.xiEpsLinearModeTerm (M : NoiseModel) {n : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (x : Fin n → T4) (a : Fin n → ℝ) (k : Z4) (ω : M.Ω) : ℝ

The corresponding real random summand at one Fourier mode.

Equations

• M.xiEpsLinearModeTerm ρ ε x a k ω = (Anderson4D.NoiseModel.xiEpsLinearModeCoeff ρ ε x a k * M.g k ω).re

noncomputable def Anderson4D.NoiseModel.xiEpsLinearCombination (M : NoiseModel) {n : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (x : Fin n → T4) (a : Fin n → ℝ) (ω : M.Ω) : ℝ

The actual finite real spatial linear combination.

Equations

• M.xiEpsLinearCombination ρ ε x a ω = ∑ i : Fin n, a i * M.xiEps ρ ε ω (x i)

noncomputable def Anderson4D.NoiseModel.xiEpsLinearCombinationFinite (M : NoiseModel) {n : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (x : Fin n → T4) (a : Fin n → ℝ) (N : ℕ) (ω : M.Ω) : ℝ

The prefix approximation to xiEpsLinearCombination.

Equations

• M.xiEpsLinearCombinationFinite ρ ε x a N ω = ∑ m ∈ Finset.range N, M.xiEpsLinearModeTerm ρ ε x a (Anderson4D.z4Enumeration m) ω

theorem Anderson4D.NoiseModel.eLpNorm_g_two (M : NoiseModel) (k : Z4) : MeasureTheory.eLpNorm (M.g k) 2 MeasureTheory.volume = 1

theorem Anderson4D.NoiseModel.eLpNorm_mul_g_two (M : NoiseModel) (c : ℂ) (k : Z4) : MeasureTheory.eLpNorm (fun (ω : M.Ω) => c * M.g k ω) 2 MeasureTheory.volume = ‖c‖ₑ

theorem Anderson4D.NoiseModel.summable_norm_xiEpsLinearModeCoeff {n : ℕ} (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (x : Fin n → T4) (a : Fin n → ℝ) : Summable fun (k : Z4) => ‖xiEpsLinearModeCoeff ρ ε x a k‖

theorem Anderson4D.NoiseModel.memLp_xiEpsLinearModeTerm (M : NoiseModel) {n : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (x : Fin n → T4) (a : Fin n → ℝ) (k : Z4) : MeasureTheory.MemLp (M.xiEpsLinearModeTerm ρ ε x a k) 2 MeasureTheory.volume

theorem Anderson4D.NoiseModel.eLpNorm_xiEpsLinearModeTerm_le (M : NoiseModel) {n : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (x : Fin n → T4) (a : Fin n → ℝ) (k : Z4) : MeasureTheory.eLpNorm (M.xiEpsLinearModeTerm ρ ε x a k) 2 MeasureTheory.volume ≤ ‖xiEpsLinearModeCoeff ρ ε x a k‖ₑ

noncomputable def Anderson4D.NoiseModel.xiEpsLinearModeLp (M : NoiseModel) {n : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (x : Fin n → T4) (a : Fin n → ℝ) (k : Z4) : ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)

One Fourier summand as an element of real L².

Equations

• M.xiEpsLinearModeLp ρ ε x a k = MeasureTheory.MemLp.toLp (M.xiEpsLinearModeTerm ρ ε x a k) ⋯

theorem Anderson4D.NoiseModel.norm_xiEpsLinearModeLp_le (M : NoiseModel) {n : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (x : Fin n → T4) (a : Fin n → ℝ) (k : Z4) : ‖M.xiEpsLinearModeLp ρ ε x a k‖ ≤ ‖xiEpsLinearModeCoeff ρ ε x a k‖

theorem Anderson4D.NoiseModel.summable_xiEpsLinearModeLp (M : NoiseModel) {n : ℕ} (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (x : Fin n → T4) (a : Fin n → ℝ) : Summable fun (k : Z4) => M.xiEpsLinearModeLp ρ ε x a k

theorem Anderson4D.NoiseModel.summable_norm_xiEpsLinearModeLp (M : NoiseModel) {n : ℕ} (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (x : Fin n → T4) (a : Fin n → ℝ) : Summable fun (k : Z4) => ‖M.xiEpsLinearModeLp ρ ε x a k‖

theorem Anderson4D.NoiseModel.xiEpsLinearCombinationFinite_eq_linearCombination (M : NoiseModel) {n : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (x : Fin n → T4) (a : Fin n → ℝ) (N : ℕ) : M.xiEpsLinearCombinationFinite ρ ε x a N = M.linearCombination (noiseModePrefix N) (fun (k : Z4) => (xiEpsLinearModeCoeff ρ ε x a k).re) fun (k : Z4) => -(xiEpsLinearModeCoeff ρ ε x a k).im

theorem Anderson4D.NoiseModel.hasGaussianLaw_xiEpsLinearCombinationFinite (M : NoiseModel) {n : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (x : Fin n → T4) (a : Fin n → ℝ) (N : ℕ) : ProbabilityTheory.HasGaussianLaw (M.xiEpsLinearCombinationFinite ρ ε x a N) MeasureTheory.volume

theorem Anderson4D.NoiseModel.integral_xiEpsLinearCombinationFinite (M : NoiseModel) {n : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (x : Fin n → T4) (a : Fin n → ℝ) (N : ℕ) : ∫ (ω : M.Ω), M.xiEpsLinearCombinationFinite ρ ε x a N ω = 0

theorem Anderson4D.NoiseModel.memLp_xiEpsLinearCombinationFinite (M : NoiseModel) {n : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (x : Fin n → T4) (a : Fin n → ℝ) (N : ℕ) : MeasureTheory.MemLp (M.xiEpsLinearCombinationFinite ρ ε x a N) 2 MeasureTheory.volume

theorem Anderson4D.NoiseModel.ae_tsum_xiEpsLinearModeTerm_eq (M : NoiseModel) {n : ℕ} (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (x : Fin n → T4) (a : Fin n → ℝ) : (fun (ω : M.Ω) => ∑' (k : Z4), M.xiEpsLinearModeTerm ρ ε x a k ω) =ᵐ[MeasureTheory.volume] M.xiEpsLinearCombination ρ ε x a

On the almost-sure absolute-convergence event, summing the combined mode terms recovers the finite spatial linear combination.

theorem Anderson4D.NoiseModel.ae_coe_tsum_xiEpsLinearModeLp_eq (M : NoiseModel) {n : ℕ} (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (x : Fin n → T4) (a : Fin n → ℝ) : ↑↑(∑' (k : Z4), M.xiEpsLinearModeLp ρ ε x a k) =ᵐ[MeasureTheory.volume] M.xiEpsLinearCombination ρ ε x a

The L² sum of the single-mode terms represents the actual finite spatial linear combination.

theorem Anderson4D.NoiseModel.memLp_xiEpsLinearCombination (M : NoiseModel) {n : ℕ} (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (x : Fin n → T4) (a : Fin n → ℝ) : MeasureTheory.MemLp (M.xiEpsLinearCombination ρ ε x a) 2 MeasureTheory.volume

theorem Anderson4D.NoiseModel.tsum_xiEpsLinearModeLp_eq_toLp (M : NoiseModel) {n : ℕ} (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (x : Fin n → T4) (a : Fin n → ℝ) : ∑' (k : Z4), M.xiEpsLinearModeLp ρ ε x a k = MeasureTheory.MemLp.toLp (M.xiEpsLinearCombination ρ ε x a) ⋯

theorem Anderson4D.NoiseModel.sum_range_xiEpsLinearModeLp_eq_toLp_finite (M : NoiseModel) {n : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (x : Fin n → T4) (a : Fin n → ℝ) (N : ℕ) : ∑ m ∈ Finset.range N, M.xiEpsLinearModeLp ρ ε x a (z4Enumeration m) = MeasureTheory.MemLp.toLp (M.xiEpsLinearCombinationFinite ρ ε x a N) ⋯

theorem Anderson4D.NoiseModel.tendsto_eLpNorm_xiEpsLinearCombinationFinite (M : NoiseModel) {n : ℕ} (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (x : Fin n → T4) (a : Fin n → ℝ) : Filter.Tendsto (fun (N : ℕ) => MeasureTheory.eLpNorm (M.xiEpsLinearCombinationFinite ρ ε x a N - M.xiEpsLinearCombination ρ ε x a) 2 MeasureTheory.volume) Filter.atTop (nhds 0)

theorem Anderson4D.NoiseModel.hasGaussianLaw_xiEpsLinearCombination (M : NoiseModel) {n : ℕ} (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (x : Fin n → T4) (a : Fin n → ℝ) : ProbabilityTheory.HasGaussianLaw (M.xiEpsLinearCombination ρ ε x a) MeasureTheory.volume

Every finite real linear combination of spatial values of the mollified field has a Gaussian law.

theorem Anderson4D.NoiseModel.integral_xiEpsLinearModeTerm (M : NoiseModel) {n : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (x : Fin n → T4) (a : Fin n → ℝ) (k : Z4) : ∫ (ω : M.Ω), M.xiEpsLinearModeTerm ρ ε x a k ω = 0

theorem Anderson4D.NoiseModel.integral_norm_xiEpsLinearModeTerm_le (M : NoiseModel) {n : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (x : Fin n → T4) (a : Fin n → ℝ) (k : Z4) : ∫ (ω : M.Ω), ‖M.xiEpsLinearModeTerm ρ ε x a k ω‖ ≤ ‖xiEpsLinearModeCoeff ρ ε x a k‖

theorem Anderson4D.NoiseModel.integral_xiEpsLinearCombination (M : NoiseModel) {n : ℕ} (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (x : Fin n → T4) (a : Fin n → ℝ) : ∫ (ω : M.Ω), M.xiEpsLinearCombination ρ ε x a ω = 0

noncomputable def Anderson4D.NoiseModel.xiEpsVector (M : NoiseModel) {n : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (x : Fin n → T4) (ω : M.Ω) : Fin n → ℝ

Finite spatial vector of mollified-field evaluations.

Equations

• M.xiEpsVector ρ ε x ω i = M.xiEps ρ ε ω (x i)

theorem Anderson4D.NoiseModel.measurable_xiEpsVector (M : NoiseModel) {n : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (x : Fin n → T4) : Measurable (M.xiEpsVector ρ ε x)

def Anderson4D.NoiseModel.xiEpsVectorDualCoeff {n : ℕ} (L : (Fin n → ℝ) →L[ℝ] ℝ) (i : Fin n) : ℝ

Coefficients of a functional on the finite spatial vector.

Equations

• Anderson4D.NoiseModel.xiEpsVectorDualCoeff L i = L fun (j : Fin n) => if i = j then 1 else 0

theorem Anderson4D.NoiseModel.apply_xiEpsVector_eq_linearCombination (M : NoiseModel) {n : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (x : Fin n → T4) (L : (Fin n → ℝ) →L[ℝ] ℝ) (ω : M.Ω) : L (M.xiEpsVector ρ ε x ω) = M.xiEpsLinearCombination ρ ε x (xiEpsVectorDualCoeff L) ω

theorem Anderson4D.NoiseModel.isGaussian_map_xiEpsVector (M : NoiseModel) {n : ℕ} (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (x : Fin n → T4) : ProbabilityTheory.IsGaussian (MeasureTheory.Measure.map (M.xiEpsVector ρ ε x) MeasureTheory.volume)

noncomputable def Anderson4D.NoiseModel.xiEpsEuclideanVector (M : NoiseModel) {n : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (x : Fin n → T4) (ω : M.Ω) : EuclideanSpace ℝ (Fin n)

The finite spatial vector in its canonical Euclidean realization.

Equations

• M.xiEpsEuclideanVector ρ ε x ω = WithLp.toLp 2 (M.xiEpsVector ρ ε x ω)

theorem Anderson4D.NoiseModel.measurable_xiEpsEuclideanVector (M : NoiseModel) {n : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (x : Fin n → T4) : Measurable (M.xiEpsEuclideanVector ρ ε x)

theorem Anderson4D.NoiseModel.isGaussian_map_xiEpsEuclideanVector (M : NoiseModel) {n : ℕ} (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (x : Fin n → T4) : ProbabilityTheory.IsGaussian (MeasureTheory.Measure.map (M.xiEpsEuclideanVector ρ ε x) MeasureTheory.volume)

theorem Anderson4D.NoiseModel.integral_xiEps (M : NoiseModel) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (z : T4) : ∫ (ω : M.Ω), M.xiEps ρ ε ω z = 0

theorem Anderson4D.NoiseModel.integral_id_map_xiEpsVector (M : NoiseModel) {n : ℕ} (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (x : Fin n → T4) : ∫ (y : Fin n → ℝ), y ∂MeasureTheory.Measure.map (M.xiEpsVector ρ ε x) MeasureTheory.volume = 0

theorem Anderson4D.NoiseModel.integral_id_map_xiEpsEuclideanVector (M : NoiseModel) {n : ℕ} (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (x : Fin n → T4) : ∫ (y : EuclideanSpace ℝ (Fin n)), y ∂MeasureTheory.Measure.map (M.xiEpsEuclideanVector ρ ε x) MeasureTheory.volume = 0