Scalar moments of finite white-noise Fourier combinations

This file turns the Cramér--Wold field in NoiseModel into a usable one-dimensional API. Every finite real linear combination of real and imaginary Fourier coordinates has its exact Gaussian law, all moments, and the usual even/odd formulas. These are the analytic inputs for the self-contained Isserlis polarization argument.

def Anderson4D.NoiseModel.linearCombination (M : NoiseModel) (s : Finset Z4) (a b : Z4 → ℝ) (ω : M.Ω) : ℝ

A finite real linear combination of the real and imaginary parts of the Fourier coefficients.

Equations

• M.linearCombination s a b ω = ∑ k ∈ s, (a k * (M.g k ω).re + b k * (M.g k ω).im)

theorem Anderson4D.NoiseModel.measurable_linearCombination (M : NoiseModel) (s : Finset Z4) (a b : Z4 → ℝ) : Measurable (M.linearCombination s a b)

theorem Anderson4D.NoiseModel.exists_law_linearCombination (M : NoiseModel) (s : Finset Z4) (a b : Z4 → ℝ) : ∃ (v : NNReal), MeasureTheory.Measure.map (M.linearCombination s a b) MeasureTheory.volume = ProbabilityTheory.gaussianReal 0 v

The exact centered-Gaussian law supplied by the NoiseModel Cramér--Wold field.

theorem Anderson4D.NoiseModel.integral_linearCombination_pow (M : NoiseModel) (s : Finset Z4) (a b : Z4 → ℝ) (v : NNReal) (hlaw : MeasureTheory.Measure.map (M.linearCombination s a b) MeasureTheory.volume = ProbabilityTheory.gaussianReal 0 v) (n : ℕ) : ∫ (ω : M.Ω), M.linearCombination s a b ω ^ n = centeredGaussianMoment v n

Transport a raw moment across an exact centered-Gaussian law.

theorem Anderson4D.NoiseModel.integrable_linearCombination_pow_of_law (M : NoiseModel) (s : Finset Z4) (a b : Z4 → ℝ) (v : NNReal) (hlaw : MeasureTheory.Measure.map (M.linearCombination s a b) MeasureTheory.volume = ProbabilityTheory.gaussianReal 0 v) (n : ℕ) : MeasureTheory.Integrable (fun (ω : M.Ω) => M.linearCombination s a b ω ^ n) MeasureTheory.volume

All powers of a finite Fourier-coordinate combination are integrable. This is recorded separately from the integral identity because later finite-sum and polarization arguments need the integrability witness.

theorem Anderson4D.NoiseModel.integrable_linearCombination_pow (M : NoiseModel) (s : Finset Z4) (a b : Z4 → ℝ) (n : ℕ) : MeasureTheory.Integrable (fun (ω : M.Ω) => M.linearCombination s a b ω ^ n) MeasureTheory.volume

Existential-free integrability wrapper using the NoiseModel law.

noncomputable def Anderson4D.NoiseModel.linearCombinationVariance (M : NoiseModel) (s : Finset Z4) (a b : Z4 → ℝ) : NNReal

The canonical variance of a finite Fourier-coordinate combination, defined by its second moment.

Equations

• M.linearCombinationVariance s a b = ⟨∫ (ω : M.Ω), M.linearCombination s a b ω ^ 2, ⋯⟩

theorem Anderson4D.NoiseModel.map_linearCombination_eq_gaussianReal (M : NoiseModel) (s : Finset Z4) (a b : Z4 → ℝ) : MeasureTheory.Measure.map (M.linearCombination s a b) MeasureTheory.volume = ProbabilityTheory.gaussianReal 0 (M.linearCombinationVariance s a b)

The existential variance in the NoiseModel interface is uniquely the second moment, so every combination has a canonical exact law.

theorem Anderson4D.NoiseModel.integral_linearCombination_sq (M : NoiseModel) (s : Finset Z4) (a b : Z4 → ℝ) : ∫ (ω : M.Ω), M.linearCombination s a b ω ^ 2 = ↑(M.linearCombinationVariance s a b)

The second moment agrees definitionally with the canonical variance.

theorem Anderson4D.NoiseModel.integral_linearCombination (M : NoiseModel) (s : Finset Z4) (a b : Z4 → ℝ) : ∫ (ω : M.Ω), M.linearCombination s a b ω = 0

Every finite Fourier-coordinate combination is centered.

theorem Anderson4D.NoiseModel.integral_linearCombination_even (M : NoiseModel) (s : Finset Z4) (a b : Z4 → ℝ) (q : ℕ) : ∫ (ω : M.Ω), M.linearCombination s a b ω ^ (2 * q) = ↑(gaussianPairingCount q) * ↑(M.linearCombinationVariance s a b) ^ q

Exact even moments in terms of the canonical second-moment variance.

theorem Anderson4D.NoiseModel.exists_integral_linearCombination_even (M : NoiseModel) (s : Finset Z4) (a b : Z4 → ℝ) (q : ℕ) : ∃ (v : NNReal), ∫ (ω : M.Ω), M.linearCombination s a b ω ^ (2 * q) = ↑(gaussianPairingCount q) * ↑v ^ q

Every finite Fourier-coordinate combination has the exact even Gaussian moments for the variance appearing in its Cramér--Wold law.

theorem Anderson4D.NoiseModel.integral_linearCombination_odd (M : NoiseModel) (s : Finset Z4) (a b : Z4 → ℝ) (q : ℕ) : ∫ (ω : M.Ω), M.linearCombination s a b ω ^ (2 * q + 1) = 0

Every odd moment of a finite Fourier-coordinate combination vanishes.