Finite Gaussian vectors extracted from the noise model

The NoiseModel interface states joint Gaussianity in Cramér--Wold form. This file packages any finite list of Fourier modes as a genuine Gaussian vector containing both real and imaginary coordinates. Repeated modes are allowed; the coefficient aggregation below is therefore useful beyond a mere reindexing lemma.

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

Both real coordinates (false) and imaginary coordinates (true) of a finite list of Fourier modes.

Equations

• M.coordinateVector k ω p = if p.2 = true then (M.g (k p.1) ω).im else (M.g (k p.1) ω).re

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

def Anderson4D.NoiseModel.coordinateDualCoeff {n : ℕ} (L : (Fin n × Bool → ℝ) →L[ℝ] ℝ) (p : Fin n × Bool) : ℝ

Coefficient of a coordinate in a continuous linear functional on the finite real coordinate space.

Equations

• Anderson4D.NoiseModel.coordinateDualCoeff L p = L fun (q : Fin n × Bool) => if p = q then 1 else 0

def Anderson4D.NoiseModel.coordinateRealWeight {n : ℕ} (k : Fin n → Z4) (L : (Fin n × Bool → ℝ) →L[ℝ] ℝ) (z : Z4) : ℝ

Aggregate all real-part coefficients belonging to the same Fourier mode. This handles repeated entries in k.

Equations

• Anderson4D.NoiseModel.coordinateRealWeight k L z = ∑ i : Fin n, if k i = z then Anderson4D.NoiseModel.coordinateDualCoeff L (i, false) else 0

def Anderson4D.NoiseModel.coordinateImagWeight {n : ℕ} (k : Fin n → Z4) (L : (Fin n × Bool → ℝ) →L[ℝ] ℝ) (z : Z4) : ℝ

Aggregate all imaginary-part coefficients belonging to the same Fourier mode.

Equations

• Anderson4D.NoiseModel.coordinateImagWeight k L z = ∑ i : Fin n, if k i = z then Anderson4D.NoiseModel.coordinateDualCoeff L (i, true) else 0

theorem Anderson4D.NoiseModel.apply_coordinateVector_eq_linearCombination (M : NoiseModel) {n : ℕ} (k : Fin n → Z4) (L : (Fin n × Bool → ℝ) →L[ℝ] ℝ) (ω : M.Ω) : L (M.coordinateVector k ω) = M.linearCombination (Finset.image k Finset.univ) (coordinateRealWeight k L) (coordinateImagWeight k L) ω

Applying a functional to the finite vector is exactly a NoiseModel.linearCombination with aggregated coefficients.

theorem Anderson4D.NoiseModel.exists_map_coordinateVector_linear_eq_gaussianReal (M : NoiseModel) {n : ℕ} (k : Fin n → Z4) (L : (Fin n × Bool → ℝ) →L[ℝ] ℝ) : ∃ (v : NNReal), MeasureTheory.Measure.map (⇑L) (MeasureTheory.Measure.map (M.coordinateVector k) MeasureTheory.volume) = ProbabilityTheory.gaussianReal 0 v

Every continuous linear functional of the finite coordinate vector has an exact centered Gaussian law.

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

The law of the finite real/imaginary coordinate vector is Gaussian.

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

The finite coordinate-vector law is centered as a vector-valued Gaussian measure.