Fixed-truncation moment assembly

This file develops paper (3.36)--(3.38) for a fixed perturbative cutoff. The first step is the reality/conjugate-mode ledger needed to turn real Cramér--Wold moments into the complex mode products controlled by Proposition 3.6.

theorem Anderson4D.conj_pmCoeff (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (α β : Z4) (ω : M.Ω) : (starRingEnd ℂ) (pmCoeff M ρ lam ε m α β ω) = pmCoeff M ρ lam ε m (-α) (-β) ω

Fourier coefficients of the real random kernel P_m obey the expected conjugate-mode identity. The statement is unconditional because the Bochner integral and complex conjugation use the same junk value 0.

structure Anderson4D.FixedTruncationAtom (s B : ℕ) : Type

One atomic choice in the expansion of a real fixed-truncation mode functional: a requested mode, a positive perturbative order, and the choice of the original or conjugate summand.

• mode : Fin s
• orderIndex : Fin B
• conjugated : Bool

@[implicit_reducible]

instance Anderson4D.instDecidableEqFixedTruncationAtom {s✝ B✝ : ℕ} : DecidableEq (FixedTruncationAtom s✝ B✝)

Equations

• Anderson4D.instDecidableEqFixedTruncationAtom = Anderson4D.instDecidableEqFixedTruncationAtom.decEq

def Anderson4D.instDecidableEqFixedTruncationAtom.decEq {s✝ B✝ : ℕ} (x✝ x✝¹ : FixedTruncationAtom s✝ B✝) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Anderson4D.instFintypeFixedTruncationAtom {s✝ B✝ : ℕ} : Fintype (FixedTruncationAtom s✝ B✝)

Equations

• Anderson4D.instFintypeFixedTruncationAtom = Fintype.ofEquiv ((_ : Fin s✝) × (_ : Fin B✝) × Bool) (Anderson4D.FixedTruncationAtom.proxyTypeEquiv s✝ B✝)

def Anderson4D.FixedTruncationAtom.equivProd (s B : ℕ) : FixedTruncationAtom s B ≃ Fin s × Fin B × Bool

Product coordinates for summing over atoms.

Equations

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

@[simp]

theorem Anderson4D.FixedTruncationAtom.equivProd_symm_apply {s B : ℕ} (p : Fin s × Fin B × Bool) : (equivProd s B).symm p = { mode := p.1, orderIndex := p.2.1, conjugated := p.2.2 }

def Anderson4D.FixedTruncationAtom.order {s B : ℕ} (a : FixedTruncationAtom s B) : ℕ

The positive perturbative order represented by an atom.

Equations

• a.order = ↑a.orderIndex + 1

theorem Anderson4D.FixedTruncationAtom.order_pos {s B : ℕ} (a : FixedTruncationAtom s B) : 1 ≤ a.order

theorem Anderson4D.FixedTruncationAtom.order_le {s B : ℕ} (a : FixedTruncationAtom s B) : a.order ≤ B

def Anderson4D.FixedTruncationAtom.modePair {s B : ℕ} (modes : Fin s → Z4 × Z4) (a : FixedTruncationAtom s B) : Z4 × Z4

Mode negation encodes conjugation of a Fourier coefficient.

Equations

• Anderson4D.FixedTruncationAtom.modePair modes a = if a.conjugated = true then (-(modes a.mode).1, -(modes a.mode).2) else modes a.mode

noncomputable def Anderson4D.FixedTruncationAtom.coeff {s B : ℕ} (c : Fin s → ℂ) (a : FixedTruncationAtom s B) : ℂ

Coefficient in the identity Re(c z) = (c z + conj(c) conj(z))/2.

Equations

• Anderson4D.FixedTruncationAtom.coeff c a = if a.conjugated = true then (starRingEnd ℂ) (c a.mode) / 2 else c a.mode / 2

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

The complex fixed-truncation scalar whose real part is used in the Cramér--Wold argument.

Equations

• Anderson4D.fixedTruncationModeSum M ρ lam ε B s modes c ω = (↑(Anderson4D.lamEps lam ε))⁻¹ * ∑ j : Fin s, c j * ∑ m : Fin B, Anderson4D.pmCoeff M ρ lam ε (↑m + 1) (modes j).1 (modes j).2 ω

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

Real scalar tested in the fixed-B moment method.

Equations

• Anderson4D.fixedTruncationReal M ρ lam ε B s modes c ω = (Anderson4D.fixedTruncationModeSum M ρ lam ε B s modes c ω).re

noncomputable def Anderson4D.fixedTruncationAtomTerm (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) {B s : ℕ} (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) (a : FixedTruncationAtom s B) (ω : M.Ω) : ℂ

One normalized complex atom in the real-part expansion.

Equations

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

theorem Anderson4D.ofReal_fixedTruncationReal_eq_sum_atoms (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (B s : ℕ) (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) (ω : M.Ω) : ↑(fixedTruncationReal M ρ lam ε B s modes c ω) = ∑ a : FixedTruncationAtom s B, fixedTruncationAtomTerm M ρ lam ε modes c a ω

Exact conjugate-mode expansion of the real fixed-truncation scalar.

theorem Anderson4D.ofReal_fixedTruncationReal_pow_eq_sum_assignments (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (B s r : ℕ) (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) (ω : M.Ω) : ↑(fixedTruncationReal M ρ lam ε B s modes c ω) ^ r = ∑ assignment : Fin r → FixedTruncationAtom s B, ∏ i : Fin r, fixedTruncationAtomTerm M ρ lam ε modes c (assignment i) ω

The r-th power of a real fixed-truncation scalar is the finite sum over all assignments of one atom to each factor.

theorem Anderson4D.prod_fixedTruncationAtomTerm (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) {B s r : ℕ} (modes : Fin s → Z4 × Z4) (c : Fin s → ℂ) (assignment : Fin r → FixedTruncationAtom s B) (ω : M.Ω) : ∏ i : Fin r, fixedTruncationAtomTerm M ρ lam ε modes c (assignment i) ω = (∏ i : Fin r, FixedTruncationAtom.coeff c (assignment i)) * (↑(lamEps lam ε))⁻¹ ^ r * ∏ i : Fin r, pmCoeff M ρ lam ε (assignment i).order (FixedTruncationAtom.modePair modes (assignment i)).1 (FixedTruncationAtom.modePair modes (assignment i)).2 ω

Pull all deterministic coefficients and normalizing powers out of one assignment product. The remaining product is exactly the random product appearing in Proposition 3.6.