Isserlis formulas for finite Fourier-noise coordinates

This file applies the abstract centered-Gaussian Isserlis theorem to the finite vectors supplied by NoiseModel.coordinateVector. The latter use the ordinary finite function space, whereas the analytic theorem is stated on Hilbert spaces. We therefore transport the vector through the canonical finite-dimensional ℓ² equivalence, prove that this transported law is Gaussian and centered, and then pull the resulting moment identities back to the original probability space.

The final Fin and List wrappers are the application-level API: arbitrary repetitions of modes and arbitrary choices of real or imaginary coordinate are allowed, every displayed product is genuinely integrable, and no moment identity is assumed.

def Anderson4D.NoiseModel.coordinateEuclideanVector (M : NoiseModel) {n : ℕ} (k : Fin n → Z4) (ω : M.Ω) : EuclideanSpace ℝ (Fin n × Bool)

The finite real/imaginary noise vector in its canonical Euclidean realization. This is only a change of norm on a finite-dimensional function space; its coordinates are definitionally those of coordinateVector.

Equations

• M.coordinateEuclideanVector k ω = WithLp.toLp 2 (M.coordinateVector k ω)

theorem Anderson4D.NoiseModel.measurable_coordinateEuclideanVector (M : NoiseModel) {n : ℕ} (k : Fin n → Z4) : Measurable (M.coordinateEuclideanVector k)

theorem Anderson4D.NoiseModel.isGaussian_map_coordinateEuclideanVector (M : NoiseModel) {n : ℕ} (k : Fin n → Z4) : ProbabilityTheory.IsGaussian (MeasureTheory.Measure.map (M.coordinateEuclideanVector k) MeasureTheory.volume)

The Euclidean realization of every finite real/imaginary coordinate vector has a genuine Gaussian law.

theorem Anderson4D.NoiseModel.integral_id_map_coordinateEuclideanVector (M : NoiseModel) {n : ℕ} (k : Fin n → Z4) : ∫ (x : EuclideanSpace ℝ (Fin n × Bool)), x ∂MeasureTheory.Measure.map (M.coordinateEuclideanVector k) MeasureTheory.volume = 0

The Euclidean finite-vector law is centered. This is transported from the exact centered law proved for coordinateVector; it is not an additional hypothesis on the noise model.

theorem Anderson4D.NoiseModel.memLp_coordinate (M : NoiseModel) {n : ℕ} (k : Fin n → Z4) (p : Fin n × Bool) (r : ENNReal) (hr : r ≠ ⊤) : MeasureTheory.MemLp (fun (ω : M.Ω) => M.coordinateVector k ω p) r MeasureTheory.volume

A selected real or imaginary Fourier coordinate has every finite Lᵖ moment.

theorem Anderson4D.NoiseModel.integral_coordinate (M : NoiseModel) {n : ℕ} (k : Fin n → Z4) (p : Fin n × Bool) : ∫ (ω : M.Ω), M.coordinateVector k ω p = 0

Every selected real or imaginary coordinate is centered.

noncomputable def Anderson4D.NoiseModel.coordinateCovariance (M : NoiseModel) {n : ℕ} (k : Fin n → Z4) (p r : Fin n × Bool) : ℝ

Covariance kernel of the finite real-coordinate presentation.

Equations

• M.coordinateCovariance k p r = ProbabilityTheory.covariance (fun (ω : M.Ω) => M.coordinateVector k ω p) (fun (ω : M.Ω) => M.coordinateVector k ω r) MeasureTheory.volume

theorem Anderson4D.NoiseModel.coordinateCovariance_eq_integral (M : NoiseModel) {n : ℕ} (k : Fin n → Z4) (p r : Fin n × Bool) : M.coordinateCovariance k p r = ∫ (ω : M.Ω), M.coordinateVector k ω p * M.coordinateVector k ω r

Since every coordinate is centered, coordinateCovariance is exactly the raw second moment.

theorem Anderson4D.NoiseModel.integrable_coordinateProduct (M : NoiseModel) {n r : ℕ} (k : Fin n → Z4) (p : Fin r → Fin n × Bool) : MeasureTheory.Integrable (fun (ω : M.Ω) => ∏ i : Fin r, M.coordinateVector k ω (p i)) MeasureTheory.volume

Any finite product of selected real/imaginary coordinates is genuinely integrable. The proof uses Gaussian Lʳ moments and finite Hölder with one exponent r for each of the r factors.

theorem Anderson4D.NoiseModel.integral_coordinateProduct_even_eq_wickPairingSum (M : NoiseModel) {n : ℕ} (k : Fin n → Z4) (q : ℕ) (p : Fin (2 * q) → Fin n × Bool) : ∫ (ω : M.Ω), ∏ i : Fin (2 * q), M.coordinateVector k ω (p i) = wickPairingSum fun (i j : Fin (2 * q)) => M.coordinateCovariance k (p i) (p j)

Even-coordinate Isserlis formula for the actual Fourier-noise sample space. Repeated modes and repeated coordinates are allowed.

theorem Anderson4D.NoiseModel.integral_coordinateProduct_odd_eq_zero (M : NoiseModel) {n : ℕ} (k : Fin n → Z4) (q : ℕ) (p : Fin (2 * q + 1) → Fin n × Bool) : ∫ (ω : M.Ω), ∏ i : Fin (2 * q + 1), M.coordinateVector k ω (p i) = 0

Every odd product of selected real/imaginary Fourier coordinates has zero expectation.

theorem Anderson4D.NoiseModel.integral_coordinateProduct_eq_wickPairingSum (M : NoiseModel) {n r : ℕ} (k : Fin n → Z4) (p : Fin r → Fin n × Bool) : ∫ (ω : M.Ω), ∏ i : Fin r, M.coordinateVector k ω (p i) = wickPairingSum fun (i j : Fin r) => M.coordinateCovariance k (p i) (p j)

Parity-free Fin wrapper. This is the direct entry point for later finite-index Wick products such as those occurring inside wickAt.

theorem Anderson4D.NoiseModel.integrable_coordinateListProduct (M : NoiseModel) {n : ℕ} (k : Fin n → Z4) (ps : List (Fin n × Bool)) : MeasureTheory.Integrable (fun (ω : M.Ω) => (List.map (fun (p : Fin n × Bool) => M.coordinateVector k ω p) ps).prod) MeasureTheory.volume

List-indexed integrability wrapper.

theorem Anderson4D.NoiseModel.integral_coordinateListProduct_eq_wickPairingList (M : NoiseModel) {n : ℕ} (k : Fin n → Z4) (ps : List (Fin n × Bool)) : ∫ (ω : M.Ω), (List.map (fun (p : Fin n × Bool) => M.coordinateVector k ω p) ps).prod = wickPairingList (M.coordinateCovariance k) ps

List-indexed form of the same identity.