Complex Isserlis formulas for Fourier noise

The analytic Isserlis theorem in NoiseIsserlis is stated for arbitrary real and imaginary coordinates of a finite Fourier vector. This file performs the finite complexification needed by the random-parametrix layer. Every complex Fourier coefficient is expanded as re + I * im; the resulting finite sum is then evaluated by the already proved real coordinate Isserlis formula.

The definition complexNoiseWickPairingSum deliberately retains both finite layers of the calculation: the outer sum chooses real or imaginary coordinates, while the inner wickPairingSum sums over full pairings. Thus it is useful without imposing circularity or independence assumptions on the complex Gaussian vector. For NoiseModel.g, its two-point contractions reduce to the exact Fourier covariance in NoiseModel.cov_pair.

def Anderson4D.NoiseModel.complexCoordinateCoefficient {n : ℕ} (σ : Fin n → Bool) : ℂ

Coefficient contributed by a choice of real (false) or imaginary (true) coordinate at every position of a complex product.

Equations

• Anderson4D.NoiseModel.complexCoordinateCoefficient σ = ∏ i : Fin n, if σ i = true then Complex.I else 1

noncomputable def Anderson4D.NoiseModel.selectedCoordinateCovariance (M : NoiseModel) {n : ℕ} (k : Fin n → Z4) (σ : Fin n → Bool) (i j : Fin n) : ℝ

The real-coordinate covariance matrix selected by σ.

Equations

• M.selectedCoordinateCovariance k σ i j = M.coordinateCovariance k (i, σ i) (j, σ j)

noncomputable def Anderson4D.NoiseModel.complexNoiseWickPairingSum (M : NoiseModel) {n : ℕ} (k : Fin n → Z4) : ℂ

Complex Wick sum obtained by expanding every complex coordinate into real and imaginary parts and applying the real Isserlis formula to each choice. The inner term is a genuine full-pairing sum.

Equations

• M.complexNoiseWickPairingSum k = ∑ σ : Fin n → Bool, Anderson4D.NoiseModel.complexCoordinateCoefficient σ * ↑(Anderson4D.wickPairingSum (M.selectedCoordinateCovariance k σ))

@[simp]

theorem Anderson4D.NoiseModel.complexCoordinateCoefficient_zero (σ : Fin 0 → Bool) : complexCoordinateCoefficient σ = 1

@[simp]

theorem Anderson4D.NoiseModel.complexNoiseWickPairingSum_zero (M : NoiseModel) (k : Fin 0 → Z4) : M.complexNoiseWickPairingSum k = 1

theorem Anderson4D.NoiseModel.product_g_eq_sum_coordinateProducts (M : NoiseModel) {n : ℕ} (k : Fin n → Z4) (ω : M.Ω) : ∏ i : Fin n, M.g (k i) ω = ∑ σ : Fin n → Bool, complexCoordinateCoefficient σ * ↑(∏ i : Fin n, M.coordinateVector k ω (i, σ i))

Pointwise expansion of a finite complex Fourier product into products of selected real/imaginary coordinates.

theorem Anderson4D.NoiseModel.integrable_g_product (M : NoiseModel) {n : ℕ} (k : Fin n → Z4) : MeasureTheory.Integrable (fun (ω : M.Ω) => ∏ i : Fin n, M.g (k i) ω) MeasureTheory.volume

Every finite product of complex Fourier coefficients is genuinely integrable.

theorem Anderson4D.NoiseModel.integral_g_product_eq_complexNoiseWickPairingSum (M : NoiseModel) {n : ℕ} (k : Fin n → Z4) : ∫ (ω : M.Ω), ∏ i : Fin n, M.g (k i) ω = M.complexNoiseWickPairingSum k

Complex Isserlis formula for an arbitrary finite family of Fourier coordinates, with repetitions allowed.

theorem Anderson4D.NoiseModel.integral_g_product_odd_eq_zero (M : NoiseModel) (q : ℕ) (k : Fin (2 * q + 1) → Z4) : ∫ (ω : M.Ω), ∏ i : Fin (2 * q + 1), M.g (k i) ω = 0

Odd complex Fourier moments vanish.

def Anderson4D.NoiseModel.twoModes (k l : Z4) : Fin 2 → Z4

The two-entry mode vector used to expose the complex contraction of the general Wick sum.

Equations

• Anderson4D.NoiseModel.twoModes k l = ![k, l]

@[simp]

theorem Anderson4D.NoiseModel.twoModes_zero (k l : Z4) : twoModes k l 0 = k

@[simp]

theorem Anderson4D.NoiseModel.twoModes_one (k l : Z4) : twoModes k l 1 = l

theorem Anderson4D.NoiseModel.complexNoiseWickPairingSum_two (M : NoiseModel) (k l : Z4) : M.complexNoiseWickPairingSum (twoModes k l) = if k = -l then 1 else 0

At order two, the complexified Wick sum is exactly the Fourier covariance contraction 1_{k=-l}.

def Anderson4D.NoiseModel.orientedMode {n : ℕ} (k : Fin n → Z4) (conjugated : Fin n → Bool) (i : Fin n) : Z4

Replace a conjugated Fourier coordinate by its negative mode, using the reality relation.

Equations

• Anderson4D.NoiseModel.orientedMode k conjugated i = if conjugated i = true then -k i else k i

def Anderson4D.NoiseModel.orientedG (M : NoiseModel) {n : ℕ} (k : Fin n → Z4) (conjugated : Fin n → Bool) (i : Fin n) (ω : M.Ω) : ℂ

A Fourier coordinate which may be conjugated independently at every position.

Equations

• M.orientedG k conjugated i ω = if conjugated i = true then (starRingEnd ℂ) (M.g (k i) ω) else M.g (k i) ω

@[simp]

theorem Anderson4D.NoiseModel.orientedG_eq_g_orientedMode (M : NoiseModel) {n : ℕ} (k : Fin n → Z4) (conjugated : Fin n → Bool) (i : Fin n) (ω : M.Ω) : M.orientedG k conjugated i ω = M.g (orientedMode k conjugated i) ω

theorem Anderson4D.NoiseModel.integral_orientedG_product_eq_complexNoiseWickPairingSum (M : NoiseModel) {n : ℕ} (k : Fin n → Z4) (conjugated : Fin n → Bool) : ∫ (ω : M.Ω), ∏ i : Fin n, M.orientedG k conjugated i ω = M.complexNoiseWickPairingSum (orientedMode k conjugated)

Isserlis formula allowing arbitrary conjugations of the Fourier coordinates. Conjugation is absorbed into mode negation before applying the complex Wick sum.

theorem Anderson4D.NoiseModel.integral_orientedG_product_odd_eq_zero (M : NoiseModel) (q : ℕ) (k : Fin (2 * q + 1) → Z4) (conjugated : Fin (2 * q + 1) → Bool) : ∫ (ω : M.Ω), ∏ i : Fin (2 * q + 1), M.orientedG k conjugated i ω = 0

Every odd product of Fourier coordinates and their conjugates has zero expectation.

theorem Anderson4D.NoiseModel.memLp_finiteNoiseCombination (M : NoiseModel) (s : Finset Z4) (a : Z4 → ℂ) (p : ENNReal) (hp : p ≠ ⊤) : MeasureTheory.MemLp (M.finiteNoiseCombination s a) p MeasureTheory.volume

Every finite complex linear combination of the Fourier coordinates has arbitrary finite Lᵖ moments.

noncomputable def Anderson4D.NoiseModel.finiteCombinationWickPairingSum (M : NoiseModel) {n : ℕ} (s : Finset Z4) (a : Fin n → Z4 → ℂ) : ℂ

Wick sum for a product of possibly different finite complex linear combinations, all written on one finite support. The outer finite sum chooses one Fourier mode from each factor.

Equations

• M.finiteCombinationWickPairingSum s a = ∑ modes : Fin n → ↥s, (∏ i : Fin n, a i ↑(modes i)) * M.complexNoiseWickPairingSum fun (i : Fin n) => ↑(modes i)

theorem Anderson4D.NoiseModel.product_finiteNoiseCombination_eq_sum (M : NoiseModel) {n : ℕ} (s : Finset Z4) (a : Fin n → Z4 → ℂ) (ω : M.Ω) : ∏ i : Fin n, M.finiteNoiseCombination s (a i) ω = ∑ modes : Fin n → ↥s, (∏ i : Fin n, a i ↑(modes i)) * ∏ i : Fin n, M.g (↑(modes i)) ω

Pointwise expansion of a product of finite complex noise combinations.

theorem Anderson4D.NoiseModel.integrable_finiteNoiseCombination_product (M : NoiseModel) {n : ℕ} (s : Finset Z4) (a : Fin n → Z4 → ℂ) : MeasureTheory.Integrable (fun (ω : M.Ω) => ∏ i : Fin n, M.finiteNoiseCombination s (a i) ω) MeasureTheory.volume

A finite product of finite complex noise combinations is integrable.

theorem Anderson4D.NoiseModel.integral_finiteNoiseCombination_product_eq_wick (M : NoiseModel) {n : ℕ} (s : Finset Z4) (a : Fin n → Z4 → ℂ) : ∫ (ω : M.Ω), ∏ i : Fin n, M.finiteNoiseCombination s (a i) ω = M.finiteCombinationWickPairingSum s a

High-order Isserlis formula for an arbitrary finite family of finite complex linear combinations of Fourier noise.