Integrability and finite covariance sums for Fourier noise

The covariance fields in NoiseModel identify the relevant integrals, but finite-sum manipulations also need genuine integrability witnesses. They are not additional assumptions: joint Gaussianity gives every finite moment. This file extracts the complex Lᵖ consequence and packages the finite covariance calculation used by the random-parametrix layer.

noncomputable def Anderson4D.NoiseModel.coordinateComplexCLM {n : ℕ} (i : Fin n) : (Fin n × Bool → ℝ) →L[ℝ] ℂ

Recover one complex coordinate from the real/imaginary finite-vector representation.

Equations

• Anderson4D.NoiseModel.coordinateComplexCLM i = ↑Complex.equivRealProdCLM.symm ∘SL (ContinuousLinearMap.proj (i, false)).prod (ContinuousLinearMap.proj (i, true))

@[simp]

theorem Anderson4D.NoiseModel.coordinateComplexCLM_apply {n : ℕ} (i : Fin n) (x : Fin n × Bool → ℝ) : (coordinateComplexCLM i) x = ↑(x (i, false)) + ↑(x (i, true)) * Complex.I

theorem Anderson4D.NoiseModel.memLp_g (M : NoiseModel) (k : Z4) (p : ENNReal) (hp : p ≠ ⊤) : MeasureTheory.MemLp (M.g k) p MeasureTheory.volume

Every complex Fourier coefficient has moments of every finite order. This is derived from the finite-dimensional Gaussian law, rather than added to NoiseModel as a redundant field.

theorem Anderson4D.NoiseModel.integrable_g_mul_g (M : NoiseModel) (k l : Z4) : MeasureTheory.Integrable (fun (ω : M.Ω) => M.g k ω * M.g l ω) MeasureTheory.volume

Products of two Fourier coefficients are integrable.

theorem Anderson4D.NoiseModel.integrable_g_mul_conj_g (M : NoiseModel) (k l : Z4) : MeasureTheory.Integrable (fun (ω : M.Ω) => M.g k ω * (starRingEnd ℂ) (M.g l ω)) MeasureTheory.volume

Products with a conjugated Fourier coefficient are integrable.

def Anderson4D.NoiseModel.finiteNoiseCombination (M : NoiseModel) (s : Finset Z4) (a : Z4 → ℂ) (ω : M.Ω) : ℂ

A finite complex linear combination of Fourier coefficients.

Equations

• M.finiteNoiseCombination s a ω = ∑ k ∈ s, a k * M.g k ω

theorem Anderson4D.NoiseModel.integrable_finiteNoiseCombination (M : NoiseModel) (s : Finset Z4) (a : Z4 → ℂ) : MeasureTheory.Integrable (M.finiteNoiseCombination s a) MeasureTheory.volume

theorem Anderson4D.NoiseModel.integral_finiteNoiseCombination_mul (M : NoiseModel) (s t : Finset Z4) (a b : Z4 → ℂ) : ∫ (ω : M.Ω), M.finiteNoiseCombination s a ω * M.finiteNoiseCombination t b ω = ∑ k ∈ s, ∑ l ∈ t, a k * b l * if k = -l then 1 else 0

Exact finite covariance expansion. Keeping the Kronecker factor explicit avoids imposing symmetry assumptions on either finite mode set.

theorem Anderson4D.NoiseModel.integral_finiteNoiseCombination_mul_conj (M : NoiseModel) (s t : Finset Z4) (a b : Z4 → ℂ) : ∫ (ω : M.Ω), M.finiteNoiseCombination s a ω * (starRingEnd ℂ) (M.finiteNoiseCombination t b ω) = ∑ k ∈ s, ∑ l ∈ t, a k * (starRingEnd ℂ) (b l) * if k = l then 1 else 0

Exact finite covariance expansion with conjugation in the second factor.