Gaussian identification of fixed-truncation moments

This file identifies the finite full-pairing limit supplied by Proposition 3.6 with the moments of one centered real Gaussian. It first regroups atom assignments by finite multilinearity, then evaluates the single constant-covariance Wick recursion.

theorem Anderson4D.fourPointHCoeff_zero_ne_zero : fourPointHCoeff 0 0 0 0 ≠ 0

The zero-mode four-point coefficient is strictly nonzero. This single test mode makes the coefficient table in (3.27) unique on every overlap of two Proposition 3.6 witnesses.

theorem Anderson4D.Prop36FullData.coeff_eq_of_le {M : NoiseModel} {ρ : SmoothCutoff} {lam : ℝ} (hlam : 0 < lam) {B₁ B₂ r₁ r₂ : ℕ} (data₁ : Prop36FullData M ρ lam B₁ r₁) (data₂ : Prop36FullData M ρ lam B₂ r₂) {m₁ m₂ : ℕ} (hm₁pos : 1 ≤ m₁) (hm₁B₁ : m₁ ≤ B₁) (hm₁B₂ : m₁ ≤ B₂) (hm₂pos : 1 ≤ m₂) (hm₂B₁ : m₂ ≤ B₁) (hm₂B₂ : m₂ ≤ B₂) : data₁.coeff m₁ m₂ = data₂.coeff m₁ m₂

Although Proposition 3.6 presents its witness after fixing B and r, the covariance asymptotic forces any two witnesses to agree on their common order range.

noncomputable def Anderson4D.fixedTruncationAtomPairLimit (X : ℕ → ℕ → ℝ) {B s : ℕ} (modes : Fin s → Z4 × Z4) (a b : FixedTruncationAtom s B) : ℂ

Limiting covariance between two atoms in the real-part expansion.

Equations

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

noncomputable def Anderson4D.fixedTruncationPairVariance (X : ℕ → ℕ → ℝ) (B : ℕ) {s : ℕ} (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) : ℂ

Variance obtained after summing every pair of atoms.

Equations

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

theorem Anderson4D.fixedTruncationPairVariance_congr {X Y : ℕ → ℕ → ℝ} {B s : ℕ} (hXY : ∀ (m₁ m₂ : ℕ), 1 ≤ m₁ → m₁ ≤ B → 1 ≤ m₂ → m₂ ≤ B → X m₁ m₂ = Y m₁ m₂) (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) : fixedTruncationPairVariance X B modes c = fixedTruncationPairVariance Y B modes c

theorem Anderson4D.Prop36FullData.fixedTruncationPairVariance_eq {M : NoiseModel} {ρ : SmoothCutoff} {lam : ℝ} (hlam : 0 < lam) {B₁ B₂ r₁ r₂ B s : ℕ} (data₁ : Prop36FullData M ρ lam B₁ r₁) (data₂ : Prop36FullData M ρ lam B₂ r₂) (hBB₁ : B ≤ B₁) (hBB₂ : B ≤ B₂) (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) : fixedTruncationPairVariance data₁.coeff B modes c = fixedTruncationPairVariance data₂.coeff B modes c

theorem Anderson4D.prop36PairLimit_assignment_eq_atomPairLimit (X : ℕ → ℕ → ℝ) {B s r : ℕ} (modes : Fin s → Z4 × Z4) (assignment : Fin r → FixedTruncationAtom s B) (i j : Fin r) : prop36PairLimit X (fixedTruncationAssignmentModes modes assignment) i j = fixedTruncationAtomPairLimit X modes (assignment i) (assignment j)

theorem Anderson4D.assignmentFullPairingSum_eq_finWickPairing (X : ℕ → ℕ → ℝ) {B s r : ℕ} (modes : Fin s → Z4 × Z4) (assignment : Fin r → FixedTruncationAtom s B) : ∑ κ : PartialPairing (Fin r) with κ.IsFull, ∏ i ∈ κ.pairSupport with i < κ i, prop36PairLimit X (fixedTruncationAssignmentModes modes assignment) i (κ i) = finWickPairing (fixedTruncationAtomPairLimit X modes) r assignment

The explicit full-pairing sum for one atom assignment is the recursive Wick sum for the atom covariance kernel.

theorem Anderson4D.fixedTruncationMomentLimit_eq_finWickPairing {M : NoiseModel} {ρ : SmoothCutoff} {lam : ℝ} {B' r : ℕ} (data : Prop36FullData M ρ lam B' r) (B : ℕ) {s : ℕ} (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) : fixedTruncationMomentLimit data B modes c = finWickPairing (fun (x x_1 : Fin r) => fixedTruncationPairVariance data.coeff B modes c) r id

All atom assignments regroup into one full-pairing sum with the summed pair variance on every edge.

theorem Anderson4D.fixedTruncationMomentLimit_two {M : NoiseModel} {ρ : SmoothCutoff} {lam : ℝ} {B' : ℕ} (data : Prop36FullData M ρ lam B' 2) (B : ℕ) {s : ℕ} (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) : fixedTruncationMomentLimit data B modes c = fixedTruncationPairVariance data.coeff B modes c

The second full-pairing limit is the summed atom covariance itself.

theorem Anderson4D.Prop36.canonicalPairVariance_real_nonneg {M : NoiseModel} {ρ : SmoothCutoff} {lam : ℝ} (hP36 : Prop36 M ρ lam) (hlam : 0 < lam) (B : ℕ) {s : ℕ} (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) : have V := fixedTruncationPairVariance (hP36.fullData B 2).coeff B modes c; V.im = 0 ∧ 0 ≤ V.re

For the canonical r=2 witness, the finite summed covariance is real and nonnegative because it is the limit of genuine real squares.

noncomputable def Anderson4D.fixedTruncationGaussianVariance {M : NoiseModel} {ρ : SmoothCutoff} {lam : ℝ} (hP36 : Prop36 M ρ lam) (hlam : 0 < lam) (B : ℕ) {s : ℕ} (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) : NNReal

Canonical nonnegative finite-truncation variance.

Equations

• Anderson4D.fixedTruncationGaussianVariance hP36 hlam B modes c = ⟨(Anderson4D.fixedTruncationPairVariance (hP36.fullData B 2).coeff B modes c).re, ⋯⟩

theorem Anderson4D.ofReal_fixedTruncationGaussianVariance {M : NoiseModel} {ρ : SmoothCutoff} {lam : ℝ} (hP36 : Prop36 M ρ lam) (hlam : 0 < lam) (B : ℕ) {s : ℕ} (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) : ↑(fixedTruncationGaussianVariance hP36 hlam B modes c) = (fixedTruncationPairVariance (hP36.fullData B 2).coeff B modes c).re

theorem Anderson4D.complex_ofReal_fixedTruncationGaussianVariance {M : NoiseModel} {ρ : SmoothCutoff} {lam : ℝ} (hP36 : Prop36 M ρ lam) (hlam : 0 < lam) (B : ℕ) {s : ℕ} (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) : ↑↑(fixedTruncationGaussianVariance hP36 hlam B modes c) = fixedTruncationPairVariance (hP36.fullData B 2).coeff B modes c

theorem Anderson4D.Prop36.fixedTruncationMomentLimit_eq_gaussianMoment {M : NoiseModel} {ρ : SmoothCutoff} {lam : ℝ} (hP36 : Prop36 M ρ lam) (hlam : 0 < lam) (B n : ℕ) {s : ℕ} (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) : fixedTruncationMomentLimit (hP36.fullData B n) B modes c = ↑(centeredGaussianMoment (fixedTruncationGaussianVariance hP36 hlam B modes c) n)

Every chosen moment-order witness gives the moments of the same canonical finite-truncation Gaussian.

theorem Anderson4D.Prop36FullData.integral_fixedTruncationComplexPow_re {M : NoiseModel} {ρ : SmoothCutoff} {lam : ℝ} {B' n : ℕ} (data : Prop36FullData M ρ lam B' n) {B s : ℕ} (hBB' : B ≤ B') (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) (ε : ℝ) : (∫ (ω : M.Ω), ↑(fixedTruncationReal M ρ lam ε B s modes c ω) ^ n).re = ∫ (ω : M.Ω), fixedTruncationReal M ρ lam ε B s modes c ω ^ n

Real part of the complexified power integral is the ordinary real raw moment.

theorem Anderson4D.Prop36.tendsto_fixedTruncationRealMoment {M : NoiseModel} {ρ : SmoothCutoff} {lam : ℝ} (hP36 : Prop36 M ρ lam) (hlam : 0 < lam) (B n : ℕ) {s : ℕ} (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) : Filter.Tendsto (fun (ε : ℝ) => ∫ (ω : M.Ω), fixedTruncationReal M ρ lam ε B s modes c ω ^ n) (nhdsWithin 0 (Set.Ioi 0)) (nhds (centeredGaussianMoment (fixedTruncationGaussianVariance hP36 hlam B modes c) n))

Fixed-B convergence of every ordinary real moment to the canonical centered Gaussian moment.

theorem Anderson4D.Prop36.aemeasurable_fixedTruncationReal {M : NoiseModel} {ρ : SmoothCutoff} {lam : ℝ} (hP36 : Prop36 M ρ lam) (B : ℕ) {s : ℕ} (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) (ε : ℝ) : AEMeasurable (fixedTruncationReal M ρ lam ε B s modes c) MeasureTheory.volume

The fixed-truncation scalar is almost-everywhere measurable, as required for its pushforward law.

theorem Anderson4D.Prop36.memLp_fixedTruncationReal {M : NoiseModel} {ρ : SmoothCutoff} {lam : ℝ} (hP36 : Prop36 M ρ lam) (B n : ℕ) {s : ℕ} (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) (ε : ℝ) : MeasureTheory.MemLp (fixedTruncationReal M ρ lam ε B s modes c) (↑n) MeasureTheory.volume

Every finite raw moment of the fixed-truncation scalar exists.

noncomputable def Anderson4D.fixedTruncationLaw (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (B s : ℕ) (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) : MeasureTheory.Measure ℝ

Pushforward law of one fixed-truncation Cramér--Wold scalar.

Equations

• Anderson4D.fixedTruncationLaw M ρ lam ε B s modes c = MeasureTheory.Measure.map (Anderson4D.fixedTruncationReal M ρ lam ε B s modes c) MeasureTheory.volume

theorem Anderson4D.Prop36.tendsto_fixedTruncationCharFun {M : NoiseModel} {ρ : SmoothCutoff} {lam : ℝ} (hP36 : Prop36 M ρ lam) (hlam : 0 < lam) (B : ℕ) {s : ℕ} (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) : Filter.Tendsto (fun (ε : ℝ) => MeasureTheory.charFun (fixedTruncationLaw M ρ lam ε B s modes c) 1) (nhdsWithin 0 (Set.Ioi 0)) (nhds (MeasureTheory.charFun (ProbabilityTheory.gaussianReal 0 (fixedTruncationGaussianVariance hP36 hlam B modes c)) 1))

Fixed-truncation convergence in law, in the characteristic-function form needed by the final two-limit argument.