Regrouping complex Wick expansions

This file proves the finite algebraic bridge from the real/imaginary expansion in complexNoiseWickPairingSum to one recursive full-pairing sum whose contractions are complex covariances. The recursion pairs the first label with one remaining label and removes both, so every labeled full pairing occurs exactly once.

A scalar-generic full-pairing recursion

def Anderson4D.finWickPairing {α : Type u_1} {R : Type u_2} [CommSemiring R] (C : α → α → R) (n : ℕ) : (Fin n → α) → R

Full-pairing sum on a finite vector. At each step the first label is paired with j.succ, and both labels are removed.

Equations

• Anderson4D.finWickPairing C 0 x_2 = 1
• Anderson4D.finWickPairing C 1 x_2 = 0
• Anderson4D.finWickPairing C n.succ.succ v = ∑ j : Fin (n + 1), C (v 0) (v j.succ) * Anderson4D.finWickPairing C n fun (i : Fin n) => v (j.succAbove i).succ

@[simp]

theorem Anderson4D.finWickPairing_zero {α : Type u_1} {R : Type u_2} [CommSemiring R] (C : α → α → R) (v : Fin 0 → α) : finWickPairing C 0 v = 1

@[simp]

theorem Anderson4D.finWickPairing_one {α : Type u_1} {R : Type u_2} [CommSemiring R] (C : α → α → R) (v : Fin 1 → α) : finWickPairing C 1 v = 0

@[simp]

theorem Anderson4D.finWickPairing_add_two {α : Type u_1} {R : Type u_2} [CommSemiring R] (C : α → α → R) (n : ℕ) (v : Fin (n + 2) → α) : finWickPairing C (n + 2) v = ∑ j : Fin (n + 1), C (v 0) (v j.succ) * finWickPairing C n fun (i : Fin n) => v (j.succAbove i).succ

theorem Anderson4D.finWickPairing_comp {α : Type u_1} {β : Type u_2} {R : Type u_3} [CommSemiring R] (C : α → α → R) (f : β → α) (n : ℕ) (v : Fin n → β) : (finWickPairing C n fun (i : Fin n) => f (v i)) = finWickPairing (fun (x y : β) => C (f x) (f y)) n v

Pulling every vertex label through a map is the same as pulling the edge kernel back through that map.

Explicit labeled full pairings

def Anderson4D.LabeledFullPairing : ℕ → Type

A recursively labeled full pairing. For n + 2 vertices, the first vertex chooses its partner in Fin (n + 1), and the tail is a full pairing of the remaining n relabeled vertices.

Equations

• Anderson4D.LabeledFullPairing 0 = PUnit.{1}
• Anderson4D.LabeledFullPairing 1 = Empty
• Anderson4D.LabeledFullPairing n.succ.succ = (Fin (n + 1) × Anderson4D.LabeledFullPairing n)

def Anderson4D.labeledFullPairingAddTwoEquiv (n : ℕ) : Fin (n + 1) × LabeledFullPairing n ≃ LabeledFullPairing (n + 2)

Constructor equivalence for a nonempty labeled full pairing.

Equations

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

@[simp]

theorem Anderson4D.labeledFullPairingAddTwoEquiv_apply (n : ℕ) (p : Fin (n + 1) × LabeledFullPairing n) : (labeledFullPairingAddTwoEquiv n) p = p

instance Anderson4D.labeledFullPairingFinite (n : ℕ) : Finite (LabeledFullPairing n)

@[implicit_reducible]

noncomputable instance Anderson4D.labeledFullPairingFintype (n : ℕ) : Fintype (LabeledFullPairing n)

Equations

• Anderson4D.labeledFullPairingFintype n = Fintype.ofFinite (Anderson4D.LabeledFullPairing n)

def Anderson4D.labeledFullPairingEdges (n : ℕ) : LabeledFullPairing n → List (Fin n × Fin n)

The edge list represented by a recursively labeled full pairing. Every vertex occurs in exactly one edge by construction.

Equations

• One or more equations did not get rendered due to their size.
• Anderson4D.labeledFullPairingEdges 0 x_2 = []

def Anderson4D.labeledFullPairingProduct {α : Type u_1} {R : Type u_2} [CommMonoid R] (C : α → α → R) (n : ℕ) : LabeledFullPairing n → (Fin n → α) → R

Product of edge contractions attached to one labeled full pairing.

Equations

• Anderson4D.labeledFullPairingProduct C x✝² x✝¹ x✝ = (List.map (fun (e : Fin x✝² × Fin x✝²) => C (x✝ e.1) (x✝ e.2)) (Anderson4D.labeledFullPairingEdges x✝² x✝¹)).prod

@[simp]

theorem Anderson4D.labeledFullPairingProduct_zero {α : Type u_1} {R : Type u_2} [CommMonoid R] (C : α → α → R) (p : LabeledFullPairing 0) (v : Fin 0 → α) : labeledFullPairingProduct C 0 p v = 1

@[simp]

theorem Anderson4D.labeledFullPairingProduct_add_two {α : Type u_1} {R : Type u_2} [CommMonoid R] (C : α → α → R) (n : ℕ) (p : LabeledFullPairing (n + 2)) (v : Fin (n + 2) → α) : labeledFullPairingProduct C (n + 2) p v = C (v 0) (v p.1.succ) * labeledFullPairingProduct C n p.2 fun (i : Fin n) => v (p.1.succAbove i).succ

noncomputable def Anderson4D.fullPairingCovarianceSum {α : Type u_1} {R : Type u_2} [CommSemiring R] (C : α → α → R) (n : ℕ) (v : Fin n → α) : R

A literal single sum over labeled full pairings, each summand being the product of the contractions on its edge list.

Equations

• Anderson4D.fullPairingCovarianceSum C n v = ∑ p : Anderson4D.LabeledFullPairing n, Anderson4D.labeledFullPairingProduct C n p v

theorem Anderson4D.fullPairingCovarianceSum_eq_finWickPairing {α : Type u_1} {R : Type u_2} [CommSemiring R] (C : α → α → R) (n : ℕ) (v : Fin n → α) : fullPairingCovarianceSum C n v = finWickPairing C n v

The explicit full-pairing sum and the head-partner recursion are equal. Thus the recursive algebra used below has no hidden multiplicity.

Cross-single interface

def Anderson4D.crossSinglesEquivCovarianceProduct {ιp : Type u_1} {ιm : Type u_2} {R : Type u_3} [Fintype ιp] [DecidableEq ιp] [Fintype ιm] [DecidableEq ιm] [CommMonoid R] (κp : PartialPairing ιp) (κm : PartialPairing ιm) (C : ↥κp.singles → ↥κm.singles → R) (π : ↥κp.singles ≃ ↥κm.singles) : R

Product of cross covariances indexed by a bijection between the single sets of two partial pairings. This is the exact indexing shape used by deterministicMomentPairingSum.

Equations

• Anderson4D.crossSinglesEquivCovarianceProduct κp κm C π = ∏ i : ↥κp.singles, C i (π i)

def Anderson4D.crossSinglesEquivCovarianceSum {ιp : Type u_1} {ιm : Type u_2} {R : Type u_3} [Fintype ιp] [DecidableEq ιp] [Fintype ιm] [DecidableEq ιm] [CommSemiring R] (κp : PartialPairing ιp) (κm : PartialPairing ιm) (C : ↥κp.singles → ↥κm.singles → R) : R

Sum over cross-single bijections. Consumers of the deterministic moment decomposition can use this without quotienting or reindexing its existing κp.singles ≃ κm.singles parameter.

Equations

• Anderson4D.crossSinglesEquivCovarianceSum κp κm C = ∑ π : ↥κp.singles ≃ ↥κm.singles, Anderson4D.crossSinglesEquivCovarianceProduct κp κm C π

theorem Anderson4D.finWickPairing_real_eq_wickPairingSum {α : Type u_1} (C : α → α → ℝ) (n : ℕ) (v : Fin n → α) : finWickPairing C n v = wickPairingSum fun (i j : Fin n) => C (v i) (v j)

The vector recursion is the existing real wickPairingSum.

Complexification and regrouping

def Anderson4D.complexChoiceCoefficient (b : Bool) : ℂ

Scalar attached to a real/imaginary choice.

Equations

• Anderson4D.complexChoiceCoefficient b = if b = true then Complex.I else 1

def Anderson4D.complexifiedCovariance {α : Type u_1} (C : α × Bool → α × Bool → ℝ) (x y : α) : ℂ

Bilinear complexification of a covariance on real/imaginary labels.

Equations

• Anderson4D.complexifiedCovariance C x y = ∑ b : Bool, ∑ c : Bool, Anderson4D.complexChoiceCoefficient b * Anderson4D.complexChoiceCoefficient c * ↑(C (x, b) (y, c))

def Anderson4D.pairChoiceEquiv {n : ℕ} (j : Fin (n + 1)) : Bool × Bool × (Fin n → Bool) ≃ (Fin (n + 2) → Bool)

Split a Boolean assignment into the choice at the head, the choice at the selected partner, and the choices at all remaining positions.

Equations

• Anderson4D.pairChoiceEquiv j = ((Equiv.refl Bool).prodCongr (Fin.insertNthEquiv (fun (x : Fin (n + 1)) => Bool) j)).trans (Fin.consEquiv fun (x : Fin (n + 2)) => Bool)

@[simp]

theorem Anderson4D.pairChoiceEquiv_zero {n : ℕ} (j : Fin (n + 1)) (b c : Bool) (τ : Fin n → Bool) : (pairChoiceEquiv j) (b, c, τ) 0 = b

@[simp]

theorem Anderson4D.pairChoiceEquiv_partner {n : ℕ} (j : Fin (n + 1)) (b c : Bool) (τ : Fin n → Bool) : (pairChoiceEquiv j) (b, c, τ) j.succ = c

@[simp]

theorem Anderson4D.pairChoiceEquiv_remaining {n : ℕ} (j : Fin (n + 1)) (b c : Bool) (τ : Fin n → Bool) (i : Fin n) : (pairChoiceEquiv j) (b, c, τ) (j.succAbove i).succ = τ i

theorem Anderson4D.complexCoordinateCoefficient_pairChoiceEquiv {n : ℕ} (j : Fin (n + 1)) (b c : Bool) (τ : Fin n → Bool) : NoiseModel.complexCoordinateCoefficient ((pairChoiceEquiv j) (b, c, τ)) = complexChoiceCoefficient b * complexChoiceCoefficient c * NoiseModel.complexCoordinateCoefficient τ

The coefficient of a split assignment factors over the selected pair and the remaining positions.

theorem Anderson4D.complexCoordinateExpansion_eq_finWickPairing {α : Type u_1} (C : α × Bool → α × Bool → ℝ) (n : ℕ) (v : Fin n → α) : ∑ σ : Fin n → Bool, NoiseModel.complexCoordinateCoefficient σ * ↑(finWickPairing C n fun (i : Fin n) => (v i, σ i)) = finWickPairing (complexifiedCovariance C) n v

Regrouping theorem: choosing real/imaginary coordinates globally and then summing real full pairings equals one complex full-pairing recursion with the bilinearly complexified covariance.

Arbitrary finite linear combinations

def Anderson4D.finiteAssignmentWeight {α : Type u_1} {β : Type u_2} {n : ℕ} (w : α → β → ℂ) (v : Fin n → α) (σ : Fin n → β) : ℂ

Weight of one global assignment of a summand to every position.

Equations

• Anderson4D.finiteAssignmentWeight w v σ = ∏ i : Fin n, w (v i) (σ i)

def Anderson4D.pairAssignmentEquiv {β : Type u_1} {n : ℕ} (j : Fin (n + 1)) : β × β × (Fin n → β) ≃ (Fin (n + 2) → β)

Split an arbitrary finite assignment at the head and its selected partner.

Equations

• Anderson4D.pairAssignmentEquiv j = ((Equiv.refl β).prodCongr (Fin.insertNthEquiv (fun (x : Fin (n + 1)) => β) j)).trans (Fin.consEquiv fun (x : Fin (n + 2)) => β)

@[simp]

theorem Anderson4D.pairAssignmentEquiv_zero {β : Type u_1} {n : ℕ} (j : Fin (n + 1)) (b c : β) (τ : Fin n → β) : (pairAssignmentEquiv j) (b, c, τ) 0 = b

@[simp]

theorem Anderson4D.pairAssignmentEquiv_partner {β : Type u_1} {n : ℕ} (j : Fin (n + 1)) (b c : β) (τ : Fin n → β) : (pairAssignmentEquiv j) (b, c, τ) j.succ = c

@[simp]

theorem Anderson4D.pairAssignmentEquiv_remaining {β : Type u_1} {n : ℕ} (j : Fin (n + 1)) (b c : β) (τ : Fin n → β) (i : Fin n) : (pairAssignmentEquiv j) (b, c, τ) (j.succAbove i).succ = τ i

theorem Anderson4D.finiteAssignmentWeight_pairAssignmentEquiv {α : Type u_1} {β : Type u_2} {n : ℕ} (w : α → β → ℂ) (v : Fin (n + 2) → α) (j : Fin (n + 1)) (b c : β) (τ : Fin n → β) : finiteAssignmentWeight w v ((pairAssignmentEquiv j) (b, c, τ)) = w (v 0) b * w (v j.succ) c * finiteAssignmentWeight w (fun (i : Fin n) => v (j.succAbove i).succ) τ

Assignment weights factor over the selected pair and the remaining positions.

theorem Anderson4D.finiteAssignmentExpansion_eq_finWickPairing {α : Type u_1} {β : Type u_2} [Fintype β] (C : α × β → α × β → ℂ) (w : α → β → ℂ) (n : ℕ) (v : Fin n → α) : (∑ σ : Fin n → β, finiteAssignmentWeight w v σ * finWickPairing C n fun (i : Fin n) => (v i, σ i)) = finWickPairing (fun (x y : α) => ∑ b : β, ∑ c : β, w x b * w y c * C (x, b) (y, c)) n v

Finite multilinearity of the full-pairing sum. Expanding one finite linear combination at every vertex and then summing full pairings equals a single full-pairing sum of the contracted covariance matrix.

Fourier-noise specialization

theorem Anderson4D.NoiseModel.complexNoiseWickPairingSum_eq_complexifiedFullPairing (M : NoiseModel) {n : ℕ} (k : Fin n → Z4) : M.complexNoiseWickPairingSum k = finWickPairing (complexifiedCovariance fun (p q : Fin n × Bool) => M.coordinateCovariance k p q) n id

The complex Fourier Wick expansion is one full-pairing recursion with the complexified real-coordinate covariance.

theorem Anderson4D.NoiseModel.complexified_coordinateCovariance_eq_fourier (M : NoiseModel) {n : ℕ} (k : Fin n → Z4) (i j : Fin n) : complexifiedCovariance (fun (p q : Fin n × Bool) => M.coordinateCovariance k p q) i j = if k i = -k j then 1 else 0

The bilinear complexification of the real/imaginary covariance matrix is the exact Fourier contraction.

noncomputable def Anderson4D.NoiseModel.fourierFullPairingSum {n : ℕ} (k : Fin n → Z4) : ℂ

Single-layer labeled full-pairing sum for Fourier contractions.

Equations

• Anderson4D.NoiseModel.fourierFullPairingSum k = Anderson4D.fullPairingCovarianceSum (fun (i j : Fin n) => if k i = -k j then 1 else 0) n id

theorem Anderson4D.NoiseModel.fourierFullPairingSum_eq_sum_edgeProducts {n : ℕ} (k : Fin n → Z4) : fourierFullPairingSum k = ∑ p : LabeledFullPairing n, labeledFullPairingProduct (fun (i j : Fin n) => if k i = -k j then 1 else 0) n p id

Expanded presentation: sum over one finite type of labeled full pairings, with each term the product of its Kronecker contractions.

theorem Anderson4D.NoiseModel.complexNoiseWickPairingSum_eq_fourierFullPairingSum (M : NoiseModel) {n : ℕ} (k : Fin n → Z4) : M.complexNoiseWickPairingSum k = fourierFullPairingSum k

The real/imaginary expansion is exactly the single-layer Fourier full-pairing sum.

theorem Anderson4D.NoiseModel.integral_g_product_eq_fourierFullPairingSum (M : NoiseModel) {n : ℕ} (k : Fin n → Z4) : ∫ (ω : M.Ω), ∏ i : Fin n, M.g (k i) ω = fourierFullPairingSum k

Direct complex Wick theorem in the Fourier contraction presentation.

Covariance form for finite complex linear combinations

noncomputable def Anderson4D.NoiseModel.finiteNoiseCombinationCovariance (M : NoiseModel) {n : ℕ} (s : Finset Z4) (a : Fin n → Z4 → ℂ) (i j : Fin n) : ℂ

The bilinear covariance (without conjugation) of two members of a finite family of Fourier-noise linear combinations.

Equations

• M.finiteNoiseCombinationCovariance s a i j = ∫ (ω : M.Ω), M.finiteNoiseCombination s (a i) ω * M.finiteNoiseCombination s (a j) ω

noncomputable def Anderson4D.NoiseModel.finiteCombinationCovarianceFullPairingSum (M : NoiseModel) {n : ℕ} (s : Finset Z4) (a : Fin n → Z4 → ℂ) : ℂ

One full-pairing sum whose edge weights are the covariances of the finite complex linear combinations.

Equations

• M.finiteCombinationCovarianceFullPairingSum s a = Anderson4D.fullPairingCovarianceSum (M.finiteNoiseCombinationCovariance s a) n id

theorem Anderson4D.NoiseModel.finiteNoiseCombinationCovariance_eq_sum (M : NoiseModel) {n : ℕ} (s : Finset Z4) (a : Fin n → Z4 → ℂ) (i j : Fin n) : M.finiteNoiseCombinationCovariance s a i j = ∑ k : ↥s, ∑ l : ↥s, a i ↑k * a j ↑l * if ↑k = -↑l then 1 else 0

The covariance of two finite combinations is the finite double Fourier contraction sum, written over the support subtype.

theorem Anderson4D.NoiseModel.finiteCombinationWickPairingSum_eq_covarianceFullPairingSum (M : NoiseModel) {n : ℕ} (s : Finset Z4) (a : Fin n → Z4 → ℂ) : M.finiteCombinationWickPairingSum s a = M.finiteCombinationCovarianceFullPairingSum s a

Regrouping for arbitrary finite complex linear combinations: the mode-assignment expansion is exactly one full-pairing covariance sum.

theorem Anderson4D.NoiseModel.integral_finiteNoiseCombination_product_eq_covarianceFullPairingSum (M : NoiseModel) {n : ℕ} (s : Finset Z4) (a : Fin n → Z4 → ℂ) : ∫ (ω : M.Ω), ∏ i : Fin n, M.finiteNoiseCombination s (a i) ω = M.finiteCombinationCovarianceFullPairingSum s a

High-order Isserlis formula for finite complex linear combinations, in covariance full-pairing form.