Raw Gaussian products as partial-pairing chaos sums

This file proves the algebraic decomposition used in paper equation (2.4). For every partial pairing, its two-cycles contribute positive covariance factors and its fixed points contribute the homogeneous Wick polynomial of the remaining variables. The fixed points are listed in the order inherited from the original finite carrier.

The proof is pointwise. Probability enters only in the final specialization to the mollified noise, where the covariance kernel is identified with etaEpsT4.

def Anderson4D.partialPairingSingleLabels {n : ℕ} {ι : Type u_1} (v : Fin n → ι) (κ : PartialPairing (Fin n)) : List ι

Labels at the fixed points of a partial pairing, in the order inherited from the ambient finite ordinal.

Equations

• Anderson4D.partialPairingSingleLabels v κ = List.map v (κ.singles.sort fun (a b : Fin n) => a ≤ b)

@[simp]

theorem Anderson4D.partialPairingSingleLabels_length {n : ℕ} {ι : Type u_1} (v : Fin n → ι) (κ : PartialPairing (Fin n)) : (partialPairingSingleLabels v κ).length = κ.singles.card

def Anderson4D.partialPairingCovarianceProduct {n : ℕ} {ι : Type u_1} (C : ι → ι → ℝ) (v : Fin n → ι) (κ : PartialPairing (Fin n)) : ℝ

Product of the covariance factors carried by the two-cycles of a partial pairing.

Equations

• Anderson4D.partialPairingCovarianceProduct C v κ = ∏ i ∈ κ.representatives, C (v i) (v (κ i))

def Anderson4D.partialPairingChaosWeight {n : ℕ} {ι : Type u_1} {Ω : Type u_2} (C : ι → ι → ℝ) (X : ι → Ω → ℝ) (v : Fin n → ι) (κ : PartialPairing (Fin n)) (ω : Ω) : ℝ

One summand in equation (2.4): positive covariance on every pair and the chaos projection of the product at the ordered singles.

Equations

• Anderson4D.partialPairingChaosWeight C X v κ ω = Anderson4D.partialPairingCovarianceProduct C v κ * Anderson4D.chaosProjProduct κ.singles.card C X (Anderson4D.partialPairingSingleLabels v κ) ω

theorem Anderson4D.partialPairingChaosWeight_eq_pairProduct_mul_wickPolynomial {n : ℕ} {ι : Type u_1} {Ω : Type u_2} (C : ι → ι → ℝ) (X : ι → Ω → ℝ) (v : Fin n → ι) (κ : PartialPairing (Fin n)) (ω : Ω) : partialPairingChaosWeight C X v κ ω = partialPairingCovarianceProduct C v κ * wickPolynomial C X (partialPairingSingleLabels v κ) ω

A marked-single equivalence local to the probability layer

def Anderson4D.ChaosDecomposition.PartialPairing.eraseSingle {α : Type u_1} [DecidableEq α] (κ : PartialPairing α) (j : α) (hj : κ j = j) : PartialPairing { i : α // i ≠ j }

Remove a specified fixed point from a partial pairing.

Equations

• Anderson4D.ChaosDecomposition.PartialPairing.eraseSingle κ j hj = { toFun := fun (i : { i : α // i ≠ j }) => ⟨κ ↑i, ⋯⟩, involutive := ⋯ }

@[simp]

theorem Anderson4D.ChaosDecomposition.PartialPairing.eraseSingle_apply_val {α : Type u_1} [DecidableEq α] (κ : PartialPairing α) (j : α) (hj : κ j = j) (i : { i : α // i ≠ j }) : ↑((eraseSingle κ j hj) i) = κ ↑i

def Anderson4D.ChaosDecomposition.PartialPairing.insertSingle {α : Type u_1} [DecidableEq α] (j : α) (κ : PartialPairing { i : α // i ≠ j }) : PartialPairing α

Restore a distinguished fixed point to a pairing of its complement.

Equations

• Anderson4D.ChaosDecomposition.PartialPairing.insertSingle j κ = { toFun := fun (i : α) => if h : i = j then j else ↑(κ ⟨i, h⟩), involutive := ⋯ }

@[simp]

theorem Anderson4D.ChaosDecomposition.PartialPairing.insertSingle_apply_eq {α : Type u_1} [DecidableEq α] (j : α) (κ : PartialPairing { i : α // i ≠ j }) : (insertSingle j κ) j = j

@[simp]

theorem Anderson4D.ChaosDecomposition.PartialPairing.insertSingle_apply_ne {α : Type u_1} [DecidableEq α] (j : α) (κ : PartialPairing { i : α // i ≠ j }) (i : α) (hi : i ≠ j) : (insertSingle j κ) i = ↑(κ ⟨i, hi⟩)

@[simp]

theorem Anderson4D.ChaosDecomposition.PartialPairing.eraseSingle_insertSingle {α : Type u_1} [DecidableEq α] (j : α) (κ : PartialPairing { i : α // i ≠ j }) : eraseSingle (insertSingle j κ) j ⋯ = κ

@[simp]

theorem Anderson4D.ChaosDecomposition.PartialPairing.insertSingle_eraseSingle {α : Type u_1} [DecidableEq α] (κ : PartialPairing α) (j : α) (hj : κ j = j) : insertSingle j (eraseSingle κ j hj) = κ

structure Anderson4D.ChaosDecomposition.PartialPairing.MarkedSingle (α : Type u_1) [Fintype α] [DecidableEq α] : Type u_1

A partial pairing together with one marked fixed point.

• pairing : PartialPairing α
• index : α
• isSingle : self.index ∈ self.pairing.singles

theorem Anderson4D.ChaosDecomposition.PartialPairing.MarkedSingle.ext {α : Type u_1} [Fintype α] [DecidableEq α] {d e : MarkedSingle α} (hpairing : d.pairing = e.pairing) (hindex : d.index = e.index) : d = e

theorem Anderson4D.ChaosDecomposition.PartialPairing.MarkedSingle.ext_iff {α : Type u_1} [Fintype α] [DecidableEq α] {d e : MarkedSingle α} : d = e ↔ d.pairing = e.pairing ∧ d.index = e.index

def Anderson4D.ChaosDecomposition.PartialPairing.markedSingleEquiv (α : Type u_1) [Fintype α] [DecidableEq α] : MarkedSingle α ≃ (j : α) × PartialPairing { i : α // i ≠ j }

Marking a single is equivalent to choosing its index and a pairing on the complementary carrier.

Equations

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

@[implicit_reducible]

noncomputable instance Anderson4D.ChaosDecomposition.PartialPairing.markedSingleFintype (α : Type u_1) [Fintype α] [DecidableEq α] : Fintype (MarkedSingle α)

Equations

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

@[reducible, inline]

abbrev Anderson4D.ChaosDecomposition.PartialPairing.RankedSingle (α : Type u_1) [Fintype α] [LinearOrder α] : Type u_1

A pairing together with the increasing rank of one of its singles.

Equations

• Anderson4D.ChaosDecomposition.PartialPairing.RankedSingle α = ((κ : Anderson4D.PartialPairing α) × Fin κ.singles.card)

def Anderson4D.ChaosDecomposition.PartialPairing.rankedSingleEquiv (α : Type u_1) [Fintype α] [LinearOrder α] : RankedSingle α ≃ MarkedSingle α

Increasing enumeration turns a ranked single into a marked single.

Equations

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

@[simp]

theorem Anderson4D.ChaosDecomposition.PartialPairing.rankedSingleEquiv_pairing {n : ℕ} (κ : PartialPairing (Fin n)) (j : Fin κ.singles.card) : ((rankedSingleEquiv (Fin n)) ⟨κ, j⟩).pairing = κ

@[simp]

theorem Anderson4D.ChaosDecomposition.PartialPairing.rankedSingleEquiv_index {n : ℕ} (κ : PartialPairing (Fin n)) (j : Fin κ.singles.card) : ((rankedSingleEquiv (Fin n)) ⟨κ, j⟩).index = (κ.singles.orderEmbOfFin ⋯) j

theorem Anderson4D.ChaosDecomposition.PartialPairing.rankedSingleEquiv_idxOf {n : ℕ} (κ : PartialPairing (Fin n)) (j : Fin κ.singles.card) : List.idxOf ((rankedSingleEquiv (Fin n)) ⟨κ, j⟩).index (κ.singles.sort fun (a b : Fin n) => a ≤ b) = ↑j

theorem Anderson4D.ChaosDecomposition.PartialPairing.sum_rankedSingle {α : Type u_1} {R : Type u_2} [Fintype α] [LinearOrder α] [AddCommMonoid R] (f : MarkedSingle α → R) : ∑ κ : PartialPairing α, ∑ j : Fin κ.singles.card, f ((rankedSingleEquiv α) ⟨κ, j⟩) = ∑ d : MarkedSingle α, f d

def Anderson4D.ChaosDecomposition.PartialPairing.headEquiv (n : ℕ) : PartialPairing (Fin n) ⊕ MarkedSingle (Fin n) ≃ PartialPairing (Fin (n + 1))

The two head branches, with contractions indexed by a pairing and one of its old singles.

Equations

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

@[simp]

theorem Anderson4D.ChaosDecomposition.PartialPairing.headEquiv_apply_creation (n : ℕ) (κ : PartialPairing (Fin n)) : (headEquiv n) (Sum.inl κ) = (PartialPairing.finHeadEquiv n).symm (Sum.inl κ)

@[simp]

theorem Anderson4D.ChaosDecomposition.PartialPairing.headEquiv_apply_contraction (n : ℕ) (d : MarkedSingle (Fin n)) : (headEquiv n) (Sum.inr d) = (PartialPairing.finHeadEquiv n).symm (Sum.inr ((markedSingleEquiv (Fin n)) d))

theorem Anderson4D.ChaosDecomposition.PartialPairing.sum_creation_contraction {R : Type u_1} [AddCommMonoid R] (n : ℕ) (f : PartialPairing (Fin (n + 1)) → R) : ∑ κ : PartialPairing (Fin n), f ((headEquiv n) (Sum.inl κ)) + ∑ d : MarkedSingle (Fin n), f ((headEquiv n) (Sum.inr d)) = ∑ κ : PartialPairing (Fin (n + 1)), f κ

Creation and marked contraction enumerate every pairing after adjoining a new zero exactly once.

@[simp]

theorem Anderson4D.ChaosDecomposition.PartialPairing.headEquiv_creation_zero (n : ℕ) (κ : PartialPairing (Fin n)) : ((headEquiv n) (Sum.inl κ)) 0 = 0

@[simp]

theorem Anderson4D.ChaosDecomposition.PartialPairing.headEquiv_creation_succ (n : ℕ) (κ : PartialPairing (Fin n)) (i : Fin n) : ((headEquiv n) (Sum.inl κ)) i.succ = (κ i).succ

@[simp]

theorem Anderson4D.ChaosDecomposition.PartialPairing.headEquiv_contraction_zero {n : ℕ} (d : MarkedSingle (Fin n)) : ((headEquiv n) (Sum.inr d)) 0 = d.index.succ

@[simp]

theorem Anderson4D.ChaosDecomposition.PartialPairing.headEquiv_contraction_partner {n : ℕ} (d : MarkedSingle (Fin n)) : ((headEquiv n) (Sum.inr d)) d.index.succ = 0

@[simp]

theorem Anderson4D.ChaosDecomposition.PartialPairing.headEquiv_contraction_succ_ne {n : ℕ} (d : MarkedSingle (Fin n)) (i : Fin n) (hi : i ≠ d.index) : ((headEquiv n) (Sum.inr d)) i.succ = (d.pairing i).succ

theorem Anderson4D.ChaosDecomposition.PartialPairing.singles_headEquiv_creation (n : ℕ) (κ : PartialPairing (Fin n)) : ((headEquiv n) (Sum.inl κ)).singles = insert 0 (Finset.map (Fin.succEmb n) κ.singles)

theorem Anderson4D.ChaosDecomposition.PartialPairing.singles_headEquiv_contraction {n : ℕ} (d : MarkedSingle (Fin n)) : ((headEquiv n) (Sum.inr d)).singles = Finset.map (Fin.succEmb n) (d.pairing.singles.erase d.index)

theorem Anderson4D.ChaosDecomposition.PartialPairing.representatives_headEquiv_creation (n : ℕ) (κ : PartialPairing (Fin n)) : ((headEquiv n) (Sum.inl κ)).representatives = Finset.map (Fin.succEmb n) κ.representatives

theorem Anderson4D.ChaosDecomposition.PartialPairing.representatives_headEquiv_contraction {n : ℕ} (d : MarkedSingle (Fin n)) : ((headEquiv n) (Sum.inr d)).representatives = insert 0 (Finset.map (Fin.succEmb n) d.pairing.representatives)

theorem Anderson4D.ChaosDecomposition.PartialPairing.singleLabels_headEquiv_creation {n : ℕ} {ι : Type u_1} (v : Fin (n + 1) → ι) (κ : PartialPairing (Fin n)) : partialPairingSingleLabels v ((headEquiv n) (Sum.inl κ)) = v 0 :: partialPairingSingleLabels (fun (i : Fin n) => v i.succ) κ

theorem Anderson4D.ChaosDecomposition.PartialPairing.sort_erase_eq_sort_erase {α : Type u_1} [LinearOrder α] (s : Finset α) (a : α) : ((s.erase a).sort fun (a b : α) => a ≤ b) = (s.sort fun (a b : α) => a ≤ b).erase a

theorem Anderson4D.ChaosDecomposition.PartialPairing.sort_erase_eq_eraseIdx_idxOf {α : Type u_1} [LinearOrder α] (s : Finset α) (a : α) (ha : a ∈ s) : (s.sort fun (a b : α) => a ≤ b).erase a = (s.sort fun (a b : α) => a ≤ b).eraseIdx (List.idxOf a (s.sort fun (a b : α) => a ≤ b))

theorem Anderson4D.ChaosDecomposition.PartialPairing.singleLabels_headEquiv_contraction {n : ℕ} {ι : Type u_1} (v : Fin (n + 1) → ι) (d : MarkedSingle (Fin n)) : partialPairingSingleLabels v ((headEquiv n) (Sum.inr d)) = (partialPairingSingleLabels (fun (i : Fin n) => v i.succ) d.pairing).eraseIdx (List.idxOf d.index (d.pairing.singles.sort fun (a b : Fin n) => a ≤ b))

theorem Anderson4D.ChaosDecomposition.PartialPairing.covarianceProduct_headEquiv_creation {n : ℕ} {ι : Type u_1} (C : ι → ι → ℝ) (v : Fin (n + 1) → ι) (κ : PartialPairing (Fin n)) : partialPairingCovarianceProduct C v ((headEquiv n) (Sum.inl κ)) = partialPairingCovarianceProduct C (fun (i : Fin n) => v i.succ) κ

theorem Anderson4D.ChaosDecomposition.PartialPairing.covarianceProduct_headEquiv_contraction {n : ℕ} {ι : Type u_1} (C : ι → ι → ℝ) (v : Fin (n + 1) → ι) (d : MarkedSingle (Fin n)) : partialPairingCovarianceProduct C v ((headEquiv n) (Sum.inr d)) = C (v 0) (v d.index.succ) * partialPairingCovarianceProduct C (fun (i : Fin n) => v i.succ) d.pairing

def Anderson4D.ChaosDecomposition.singleLabelRankEquiv {n : ℕ} {ι : Type u_1} (v : Fin n → ι) (κ : PartialPairing (Fin n)) : Fin κ.singles.card ≃ Fin (partialPairingSingleLabels v κ).length

Cast an increasing single rank to the definitionally equal length of the ordered single-label list.

Equations

• Anderson4D.ChaosDecomposition.singleLabelRankEquiv v κ = finCongr ⋯

@[simp]

theorem Anderson4D.ChaosDecomposition.singleLabelRankEquiv_val {n : ℕ} {ι : Type u_1} (v : Fin n → ι) (κ : PartialPairing (Fin n)) (j : Fin κ.singles.card) : ↑((singleLabelRankEquiv v κ) j) = ↑j

theorem Anderson4D.ChaosDecomposition.singleLabels_get_rank {n : ℕ} {ι : Type u_1} (v : Fin n → ι) (κ : PartialPairing (Fin n)) (j : Fin κ.singles.card) : (partialPairingSingleLabels v κ).get ((singleLabelRankEquiv v κ) j) = v ((κ.singles.orderEmbOfFin ⋯) j)

theorem Anderson4D.ChaosDecomposition.singleLabels_headEquiv_rankedContraction {n : ℕ} {ι : Type u_1} (v : Fin (n + 1) → ι) (κ : PartialPairing (Fin n)) (j : Fin κ.singles.card) : partialPairingSingleLabels v ((PartialPairing.headEquiv n) (Sum.inr ((PartialPairing.rankedSingleEquiv (Fin n)) ⟨κ, j⟩))) = (partialPairingSingleLabels (fun (i : Fin n) => v i.succ) κ).eraseIdx ↑j

theorem Anderson4D.ChaosDecomposition.covarianceProduct_headEquiv_rankedContraction {n : ℕ} {ι : Type u_1} (C : ι → ι → ℝ) (v : Fin (n + 1) → ι) (κ : PartialPairing (Fin n)) (j : Fin κ.singles.card) : partialPairingCovarianceProduct C v ((PartialPairing.headEquiv n) (Sum.inr ((PartialPairing.rankedSingleEquiv (Fin n)) ⟨κ, j⟩))) = C (v 0) (v ((κ.singles.orderEmbOfFin ⋯) j).succ) * partialPairingCovarianceProduct C (fun (i : Fin n) => v i.succ) κ

theorem Anderson4D.ChaosDecomposition.partialPairingChaosWeight_headEquiv_creation {n : ℕ} {ι : Type u_1} {Ω : Type u_2} (C : ι → ι → ℝ) (X : ι → Ω → ℝ) (v : Fin (n + 1) → ι) (κ : PartialPairing (Fin n)) (ω : Ω) : partialPairingChaosWeight C X v ((PartialPairing.headEquiv n) (Sum.inl κ)) ω = partialPairingCovarianceProduct C (fun (i : Fin n) => v i.succ) κ * wickPolynomial C X (v 0 :: partialPairingSingleLabels (fun (i : Fin n) => v i.succ) κ) ω

theorem Anderson4D.ChaosDecomposition.partialPairingChaosWeight_headEquiv_rankedContraction {n : ℕ} {ι : Type u_1} {Ω : Type u_2} (C : ι → ι → ℝ) (X : ι → Ω → ℝ) (v : Fin (n + 1) → ι) (κ : PartialPairing (Fin n)) (j : Fin κ.singles.card) (ω : Ω) : partialPairingChaosWeight C X v ((PartialPairing.headEquiv n) (Sum.inr ((PartialPairing.rankedSingleEquiv (Fin n)) ⟨κ, j⟩))) ω = C (v 0) (v ((κ.singles.orderEmbOfFin ⋯) j).succ) * partialPairingCovarianceProduct C (fun (i : Fin n) => v i.succ) κ * wickPolynomial C X ((partialPairingSingleLabels (fun (i : Fin n) => v i.succ) κ).eraseIdx ↑j) ω

theorem Anderson4D.ChaosDecomposition.sum_ranked_contractions_eq_wick_contractions {n : ℕ} {ι : Type u_1} {Ω : Type u_2} (C : ι → ι → ℝ) (X : ι → Ω → ℝ) (v : Fin (n + 1) → ι) (κ : PartialPairing (Fin n)) (ω : Ω) : ∑ j : Fin κ.singles.card, C (v 0) (v ((κ.singles.orderEmbOfFin ⋯) j).succ) * wickPolynomial C X ((partialPairingSingleLabels (fun (i : Fin n) => v i.succ) κ).eraseIdx ↑j) ω = ∑ j : Fin (partialPairingSingleLabels (fun (i : Fin n) => v i.succ) κ).length, C (v 0) ((partialPairingSingleLabels (fun (i : Fin n) => v i.succ) κ).get j) * wickPolynomial C X ((partialPairingSingleLabels (fun (i : Fin n) => v i.succ) κ).eraseIdx ↑j) ω

theorem Anderson4D.ChaosDecomposition.mul_partialPairingChaosWeight_eq_head_sum {n : ℕ} {ι : Type u_1} {Ω : Type u_2} (C : ι → ι → ℝ) (X : ι → Ω → ℝ) (v : Fin (n + 1) → ι) (κ : PartialPairing (Fin n)) (ω : Ω) : X (v 0) ω * partialPairingChaosWeight C X (fun (i : Fin n) => v i.succ) κ ω = partialPairingChaosWeight C X v ((PartialPairing.headEquiv n) (Sum.inl κ)) ω + ∑ j : Fin κ.singles.card, partialPairingChaosWeight C X v ((PartialPairing.headEquiv n) (Sum.inr ((PartialPairing.rankedSingleEquiv (Fin n)) ⟨κ, j⟩))) ω

One tail pairing obeys the creation--contraction split after adjoining the new first variable.

theorem Anderson4D.rawProduct_eq_sum_partialPairingChaos {ι : Type u_1} {Ω : Type u_2} (C : ι → ι → ℝ) (X : ι → Ω → ℝ) {n : ℕ} (v : Fin n → ι) (ω : Ω) : ∏ i : Fin n, X (v i) ω = ∑ κ : PartialPairing (Fin n), partialPairingChaosWeight C X v κ ω

Raw-product partial-pairing decomposition (paper (2.4)).

Every two-cycle contributes one positive covariance factor. The fixed points, in their original carrier order, contribute the chaos projection of degree equal to their number.

theorem Anderson4D.listProduct_eq_sum_partialPairingChaos {ι : Type u_1} {Ω : Type u_2} (C : ι → ι → ℝ) (X : ι → Ω → ℝ) (xs : List ι) (ω : Ω) : (List.map (fun (x : ι) => X x ω) xs).prod = ∑ κ : PartialPairing (Fin xs.length), partialPairingChaosWeight C X xs.get κ ω

List form of the raw-product decomposition.

theorem Anderson4D.NoiseModel.xiEpsProduct_eq_sum_partialPairingChaos (M : NoiseModel) (ρ : SmoothCutoff) {ε : ℝ} (_hε : 0 < ε) {n : ℕ} (z : Fin n → T4) (ω : M.Ω) : ∏ i : Fin n, M.xiEps ρ ε ω (z i) = ∑ κ : PartialPairing (Fin n), (∏ i ∈ κ.representatives, ρ.etaEpsT4 ε (z i - z (κ i))) * chaosProjProduct κ.singles.card (fun (x y : T4) => ρ.etaEpsT4 ε (x - y)) (fun (x : T4) (ω' : M.Ω) => M.xiEps ρ ε ω' x) (partialPairingSingleLabels z κ) ω

Equation (2.4) specialized to the mollified noise. The covariance factors have the positive sign, and the singles retain their ambient order. For positive ε, integral_xiEps_mul_eq_etaEpsT4 identifies the displayed kernel with the actual two-point covariance.