Finite Fourier approximations of the mollified noise

Before passing to the infinite random Fourier series, all covariance and moment manipulations are finite. This file records those exact identities with the project's cutoff and character normalizations.

def Anderson4D.NoiseModel.NegClosedModes (s : Finset Z4) : Prop

A finite mode set closed under the reality involution k ↦ -k.

Equations

• Anderson4D.NoiseModel.NegClosedModes s = ∀ k ∈ s, -k ∈ s

def Anderson4D.NoiseModel.negClosedModesEquiv (s : Finset Z4) (hs : NegClosedModes s) : ↥s ≃ ↥s

Negation permutes a finite negation-closed mode set.

Equations

• Anderson4D.NoiseModel.negClosedModesEquiv s hs = { toFun := fun (k : ↥s) => ⟨-↑k, ⋯⟩, invFun := fun (k : ↥s) => ⟨-↑k, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

theorem Anderson4D.NoiseModel.sum_neg_eq_sum_of_negClosedModes (s : Finset Z4) (hs : NegClosedModes s) (f : Z4 → ℂ) : ∑ k ∈ s, f (-k) = ∑ k ∈ s, f k

noncomputable def Anderson4D.NoiseModel.mollifiedModeCoeff (ρ : SmoothCutoff) (ε : ℝ) (x : T4) (k : Z4) : ℂ

Deterministic coefficient multiplying the white-noise mode g k at the spatial point x.

Equations

• Anderson4D.NoiseModel.mollifiedModeCoeff ρ ε x k = ↑Anderson4D.NoiseModel.whiteNoiseFourierScale * ρ.symbol ε k * Anderson4D.charT4 k x

noncomputable def Anderson4D.NoiseModel.xiEpsFiniteC (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (s : Finset Z4) (ω : M.Ω) (x : T4) : ℂ

Finite complex Fourier approximation to the mollified noise.

Equations

• M.xiEpsFiniteC ρ ε s ω x = M.finiteNoiseCombination s (Anderson4D.NoiseModel.mollifiedModeCoeff ρ ε x) ω

theorem Anderson4D.NoiseModel.measurable_xiEpsFiniteC (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (s : Finset Z4) (x : T4) : Measurable fun (ω : M.Ω) => M.xiEpsFiniteC ρ ε s ω x

theorem Anderson4D.NoiseModel.memLp_xiEpsFiniteC (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (s : Finset Z4) (x : T4) (p : ENNReal) (hp : p ≠ ⊤) : MeasureTheory.MemLp (fun (ω : M.Ω) => M.xiEpsFiniteC ρ ε s ω x) p MeasureTheory.volume

Every finite Fourier approximation has all finite moments.

theorem Anderson4D.NoiseModel.conj_xiEpsFiniteC_eq (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (s : Finset Z4) (hs : NegClosedModes s) (ω : M.Ω) (x : T4) : (starRingEnd ℂ) (M.xiEpsFiniteC ρ ε s ω x) = M.xiEpsFiniteC ρ ε s ω x

A negation-closed truncation is pointwise real.

theorem Anderson4D.NoiseModel.xiEpsFiniteC_im_eq_zero (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (s : Finset Z4) (hs : NegClosedModes s) (ω : M.Ω) (x : T4) : (M.xiEpsFiniteC ρ ε s ω x).im = 0

The imaginary part of a negation-closed truncation vanishes.

theorem Anderson4D.NoiseModel.integral_xiEpsFiniteC_mul (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (s t : Finset Z4) (x y : T4) : ∫ (ω : M.Ω), M.xiEpsFiniteC ρ ε s ω x * M.xiEpsFiniteC ρ ε t ω y = ∑ k ∈ s, ∑ l ∈ t, mollifiedModeCoeff ρ ε x k * mollifiedModeCoeff ρ ε y l * if k = -l then 1 else 0

The exact finite covariance, with no symmetry assumption on either mode set.

theorem Anderson4D.NoiseModel.integral_xiEpsFiniteC_mul_of_negClosedModes (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (s : Finset Z4) (hs : NegClosedModes s) (x y : T4) : ∫ (ω : M.Ω), M.xiEpsFiniteC ρ ε s ω x * M.xiEpsFiniteC ρ ε s ω y = ∑ k ∈ s, mollifiedModeCoeff ρ ε x k * mollifiedModeCoeff ρ ε y (-k)

On a negation-closed truncation, the two-field covariance collapses from a double Kronecker sum to one sum over paired modes.

theorem Anderson4D.NoiseModel.integral_xiEpsFiniteC_mul_conj (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (s t : Finset Z4) (x y : T4) : ∫ (ω : M.Ω), M.xiEpsFiniteC ρ ε s ω x * (starRingEnd ℂ) (M.xiEpsFiniteC ρ ε t ω y) = ∑ k ∈ s, ∑ l ∈ t, mollifiedModeCoeff ρ ε x k * (starRingEnd ℂ) (mollifiedModeCoeff ρ ε y l) * if k = l then 1 else 0

The exact finite covariance against a conjugated field.

noncomputable def Anderson4D.NoiseModel.xiEpsFinite (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (s : Finset Z4) (ω : M.Ω) (x : T4) : ℝ

Real part of the finite Fourier approximation, matching the codomain of the totalized infinite field xiEps.

Equations

• M.xiEpsFinite ρ ε s ω x = (M.xiEpsFiniteC ρ ε s ω x).re

theorem Anderson4D.NoiseModel.measurable_xiEpsFinite (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (s : Finset Z4) (x : T4) : Measurable fun (ω : M.Ω) => M.xiEpsFinite ρ ε s ω x

theorem Anderson4D.NoiseModel.memLp_xiEpsFinite (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (s : Finset Z4) (x : T4) (p : ENNReal) (hp : p ≠ ⊤) : MeasureTheory.MemLp (fun (ω : M.Ω) => M.xiEpsFinite ρ ε s ω x) p MeasureTheory.volume