Construction of the Fourier white-noise model

This module realizes the interface in Probability.Noise on a genuine probability space. The underlying coordinates are an independent family of standard real Gaussian random variables. An encoding-dependent fundamental domain for k ↦ -k is used only to choose which member of each two-point orbit receives the positive imaginary coordinate.

@[reducible, inline]

abbrev Anderson4D.NoiseGenerator : Type

Two real Gaussian generators are reserved for every nonzero {k,-k} orbit. The unused duplicate coordinates make the ambient product space especially simple; coefficients only read the canonical orbit representative.

Equations

• Anderson4D.NoiseGenerator = (Anderson4D.Z4 × Bool)

def Anderson4D.noiseOrbitRep (k : Z4) : Z4

An encoding-dependent representative of the orbit {k,-k}.

Equations

• Anderson4D.noiseOrbitRep k = if Encodable.encode k ≤ Encodable.encode (-k) then k else -k

def Anderson4D.noiseOrbitSign (k : Z4) : ℝ

The sign of the imaginary coordinate. It is zero at the zero mode and changes sign under k ↦ -k away from zero.

Equations

• Anderson4D.noiseOrbitSign k = if k = 0 then 0 else if Encodable.encode k ≤ Encodable.encode (-k) then 1 else -1

@[simp]

theorem Anderson4D.noiseOrbitRep_neg (k : Z4) : noiseOrbitRep (-k) = noiseOrbitRep k

@[simp]

theorem Anderson4D.noiseOrbitSign_zero : noiseOrbitSign 0 = 0

@[simp]

theorem Anderson4D.noiseOrbitSign_neg (k : Z4) : noiseOrbitSign (-k) = -noiseOrbitSign k

theorem Anderson4D.noiseOrbitRep_eq_self_or_neg (k : Z4) : noiseOrbitRep k = k ∨ noiseOrbitRep k = -k

theorem Anderson4D.noiseOrbitRep_eq_iff (k l : Z4) : noiseOrbitRep k = noiseOrbitRep l ↔ l = k ∨ l = -k

structure Anderson4D.StandardGaussianFamily : Type 1

A genuine probability space carrying mutually independent standard real Gaussian coordinates.

• Ω : Type

  Sample space.

• measureSpace : MeasureTheory.MeasureSpace self.Ω

  Probability measure, exposed as volume.

• isProbabilityMeasure : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

  The coordinate product measure is a probability measure.

• X : NoiseGenerator → self.Ω → ℝ

  Independent standard Gaussian coordinates.

• measurable_X (i : NoiseGenerator) : Measurable (self.X i)
• hasLaw_X (i : NoiseGenerator) : ProbabilityTheory.HasLaw (self.X i) (ProbabilityTheory.gaussianReal 0 1) MeasureTheory.volume
• indep_X : ProbabilityTheory.iIndepFun self.X MeasureTheory.volume

theorem Anderson4D.nonempty_standardGaussianFamily : Nonempty StandardGaussianFamily

The countable product theorem constructs the required real Gaussian family without any extra postulate.

noncomputable def Anderson4D.canonicalStandardGaussianFamily : StandardGaussianFamily

A fixed countable product of standard real Gaussian laws.

Equations

• Anderson4D.canonicalStandardGaussianFamily = Classical.choice Anderson4D.nonempty_standardGaussianFamily

theorem Anderson4D.StandardGaussianFamily.isGaussianProcess_X (F : StandardGaussianFamily) : ProbabilityTheory.IsGaussianProcess F.X MeasureTheory.volume

Every finite subfamily of the product coordinates is jointly Gaussian.

@[simp]

theorem Anderson4D.StandardGaussianFamily.integral_X (F : StandardGaussianFamily) (i : NoiseGenerator) : ∫ (ω : F.Ω), F.X i ω = 0

Every generator is centered.

@[simp]

theorem Anderson4D.StandardGaussianFamily.integral_X_sq (F : StandardGaussianFamily) (i : NoiseGenerator) : ∫ (ω : F.Ω), F.X i ω ^ 2 = 1

Every generator has variance and second moment one.

theorem Anderson4D.StandardGaussianFamily.integral_X_mul_X (F : StandardGaussianFamily) (i j : NoiseGenerator) : ∫ (ω : F.Ω), F.X i ω * F.X j ω = if i = j then 1 else 0

Distinct product coordinates are orthogonal in L²; equal coordinates have second moment one.

noncomputable def Anderson4D.noiseRealScale (k : Z4) : ℝ

Real-coordinate normalization: one at the real zero mode and 1 / √2 on nonzero orbit pairs.

Equations

• Anderson4D.noiseRealScale k = if k = 0 then 1 else 1 / √2

noncomputable def Anderson4D.noiseImagScale (k : Z4) : ℝ

Imaginary-coordinate normalization and orientation.

Equations

• Anderson4D.noiseImagScale k = if k = 0 then 0 else Anderson4D.noiseOrbitSign k / √2

@[simp]

theorem Anderson4D.noiseRealScale_neg (k : Z4) : noiseRealScale (-k) = noiseRealScale k

@[simp]

theorem Anderson4D.noiseImagScale_neg (k : Z4) : noiseImagScale (-k) = -noiseImagScale k

theorem Anderson4D.noiseScale_sq_add (k : Z4) : noiseRealScale k ^ 2 + noiseImagScale k ^ 2 = 1

theorem Anderson4D.noiseScale_sq_sub_of_ne {k : Z4} (hk : k ≠ 0) : noiseRealScale k ^ 2 - noiseImagScale k ^ 2 = 0

noncomputable def Anderson4D.StandardGaussianFamily.fourierCoeff (F : StandardGaussianFamily) (k : Z4) (ω : F.Ω) : ℂ

Fourier coefficient assembled from the two real Gaussian generators of the canonical ±k orbit.

Equations

• F.fourierCoeff k ω = { re := Anderson4D.noiseRealScale k * F.X (Anderson4D.noiseOrbitRep k, false) ω, im := Anderson4D.noiseImagScale k * F.X (Anderson4D.noiseOrbitRep k, true) ω }

theorem Anderson4D.StandardGaussianFamily.measurable_fourierCoeff (F : StandardGaussianFamily) (k : Z4) : Measurable (F.fourierCoeff k)

theorem Anderson4D.StandardGaussianFamily.fourierCoeff_neg (F : StandardGaussianFamily) (k : Z4) (ω : F.Ω) : F.fourierCoeff (-k) ω = (starRingEnd ℂ) (F.fourierCoeff k ω)

The orbit orientation gives the Fourier reality constraint pointwise, not merely almost surely.

theorem Anderson4D.StandardGaussianFamily.integrable_X_mul_X (F : StandardGaussianFamily) (i j : NoiseGenerator) : MeasureTheory.Integrable (fun (ω : F.Ω) => F.X i ω * F.X j ω) MeasureTheory.volume

Products of any two real product coordinates are integrable.

theorem Anderson4D.StandardGaussianFamily.integrable_const_mul_X_mul_X (F : StandardGaussianFamily) (c : ℝ) (i j : NoiseGenerator) : MeasureTheory.Integrable (fun (ω : F.Ω) => c * (F.X i ω * F.X j ω)) MeasureTheory.volume

A scalar multiple of a coordinate product is integrable.

theorem Anderson4D.StandardGaussianFamily.integral_const_mul_X_mul_X (F : StandardGaussianFamily) (c : ℝ) (i j : NoiseGenerator) : ∫ (ω : F.Ω), c * (F.X i ω * F.X j ω) = c * if i = j then 1 else 0

A scalar multiple of a coordinate product integrates according to the Kronecker covariance of the product family.

theorem Anderson4D.StandardGaussianFamily.integrable_fourierCoeff_mul (F : StandardGaussianFamily) (k l : Z4) : MeasureTheory.Integrable (fun (ω : F.Ω) => F.fourierCoeff k ω * F.fourierCoeff l ω) MeasureTheory.volume

The product of any two Fourier coefficients is integrable.

theorem Anderson4D.StandardGaussianFamily.integral_fourierCoeff_mul (F : StandardGaussianFamily) (k l : Z4) : ∫ (ω : F.Ω), F.fourierCoeff k ω * F.fourierCoeff l ω = ↑((noiseRealScale k * noiseRealScale l - noiseImagScale k * noiseImagScale l) * if noiseOrbitRep k = noiseOrbitRep l then 1 else 0)

Before the final orbit arithmetic, the covariance of two Fourier coefficients is the scalar covariance of their common orbit.

theorem Anderson4D.StandardGaussianFamily.fourierCovarianceScalar (k l : Z4) : ((noiseRealScale k * noiseRealScale l - noiseImagScale k * noiseImagScale l) * if noiseOrbitRep k = noiseOrbitRep l then 1 else 0) = if k = -l then 1 else 0

The orbit normalization is exactly the Fourier white-noise Kronecker covariance.

theorem Anderson4D.StandardGaussianFamily.fourierCoeff_cov_pair (F : StandardGaussianFamily) (k l : Z4) : ∫ (ω : F.Ω), F.fourierCoeff k ω * F.fourierCoeff l ω = if k = -l then 1 else 0

Exact covariance E[gₖ gₗ] = 1_{k=-l}.

theorem Anderson4D.StandardGaussianFamily.fourierCoeff_cov_conj (F : StandardGaussianFamily) (k l : Z4) : ∫ (ω : F.Ω), F.fourierCoeff k ω * (starRingEnd ℂ) (F.fourierCoeff l ω) = if k = l then 1 else 0

Exact conjugated covariance, obtained from the pointwise reality constraint and the preceding pair covariance.

def Anderson4D.StandardGaussianFamily.noiseGeneratorSet (s : Finset Z4) : Finset NoiseGenerator

The finite set of independent real coordinates read by a finite set of Fourier modes.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Anderson4D.StandardGaussianFamily.noiseFiniteCombinationCLM (s : Finset Z4) (a b : Z4 → ℝ) : (↥(noiseGeneratorSet s) → ℝ) →L[ℝ] ℝ

The continuous linear functional on the finite coordinate vector that realizes a prescribed Fourier-coordinate combination.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Anderson4D.StandardGaussianFamily.fourierLinearCombination (F : StandardGaussianFamily) (s : Finset Z4) (a b : Z4 → ℝ) (ω : F.Ω) : ℝ

The exact real combination appearing in the NoiseModel interface.

Equations

• F.fourierLinearCombination s a b ω = ∑ k ∈ s, (a k * (F.fourierCoeff k ω).re + b k * (F.fourierCoeff k ω).im)

theorem Anderson4D.StandardGaussianFamily.integrable_fourierCoeff_re (F : StandardGaussianFamily) (k : Z4) : MeasureTheory.Integrable (fun (ω : F.Ω) => (F.fourierCoeff k ω).re) MeasureTheory.volume

theorem Anderson4D.StandardGaussianFamily.integrable_fourierCoeff_im (F : StandardGaussianFamily) (k : Z4) : MeasureTheory.Integrable (fun (ω : F.Ω) => (F.fourierCoeff k ω).im) MeasureTheory.volume

@[simp]

theorem Anderson4D.StandardGaussianFamily.integral_fourierCoeff_re (F : StandardGaussianFamily) (k : Z4) : ∫ (ω : F.Ω), (F.fourierCoeff k ω).re = 0

@[simp]

theorem Anderson4D.StandardGaussianFamily.integral_fourierCoeff_im (F : StandardGaussianFamily) (k : Z4) : ∫ (ω : F.Ω), (F.fourierCoeff k ω).im = 0

theorem Anderson4D.StandardGaussianFamily.integrable_fourierLinearCombination (F : StandardGaussianFamily) (s : Finset Z4) (a b : Z4 → ℝ) : MeasureTheory.Integrable (F.fourierLinearCombination s a b) MeasureTheory.volume

Every finite real Fourier-coordinate combination is integrable.

@[simp]

theorem Anderson4D.StandardGaussianFamily.integral_fourierLinearCombination (F : StandardGaussianFamily) (s : Finset Z4) (a b : Z4 → ℝ) : ∫ (ω : F.Ω), F.fourierLinearCombination s a b ω = 0

Every finite real Fourier-coordinate combination is centered.

theorem Anderson4D.StandardGaussianFamily.hasGaussianLaw_fourierLinearCombination (F : StandardGaussianFamily) (s : Finset Z4) (a b : Z4 → ℝ) : ProbabilityTheory.HasGaussianLaw (F.fourierLinearCombination s a b) MeasureTheory.volume

The finite combination is a Gaussian random variable because it is a linear image of a finite subvector of the independent Gaussian product.

theorem Anderson4D.StandardGaussianFamily.exists_map_fourierLinearCombination_eq_gaussianReal (F : StandardGaussianFamily) (s : Finset Z4) (a b : Z4 → ℝ) : ∃ (v : NNReal), MeasureTheory.Measure.map (F.fourierLinearCombination s a b) MeasureTheory.volume = ProbabilityTheory.gaussianReal 0 v

Exact centered Gaussian pushforward law, in the shape required by NoiseModel.gaussian_lincomb.

noncomputable def Anderson4D.canonicalNoiseModel : NoiseModel

The canonical countable product construction realizes the complete NoiseModel interface.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.nonempty_noiseModel : Nonempty NoiseModel

In particular, the NoiseModel interface is inhabited without adding a postulate or treating its specification as a certificate.