The paired-head branch of the parametrix identity

This module isolates the exact deterministic and Wick ledgers for a Wick contraction. The only combinatorial datum used by the closed-form factorization is that deleting the paired head shifts every extracted interval down by one. For paper case (2), this datum is forced by the absence of a fully paired head prefix; case (3) is handled separately by the non-split prefix decomposition.

def Anderson4D.PartialPairing.ContractionExtractCompatible {n : ℕ} (d : MarkedSingle (Fin n)) : Prop

Exact extraction compatibility expected in paper case (2): after deleting the paired head, every extracted interval is shifted by one and no terminal head interval is created.

Equations

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

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

The singles of a contracted pairing are the shifted old singles with the marked partner removed.

theorem Anderson4D.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

Sorting after erasing a member is the same as erasing it from the sorted list.

theorem Anderson4D.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))

On a nodup sorted finset list, erasing a member agrees with erasing the entry at its idxOf.

theorem Anderson4D.PartialPairing.wickAtSingleLabels_wickHeadEquiv_contraction {n : ℕ} (d : MarkedSingle (Fin n)) (xt : Fin (n + 3) → T4) : wickAtSingleLabels ((wickHeadEquiv n) (Sum.inr d)) xt = (wickAtSingleLabels d.pairing (ambientTailTuple ⋯ xt)).eraseIdx (List.idxOf d.index (d.pairing.singles.sort fun (a b : Fin n) => a ≤ b))

The Wick labels of a contracted pairing are the old Wick labels with the marked partner removed at its ordered rank.

@[simp]

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

Reindexing a ranked single preserves the underlying pairing.

@[simp]

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

The marked index obtained from a rank is the increasing single enumeration at that rank.

theorem Anderson4D.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

Converting a ranked single to a marked single and then locating it in the sorted single list returns the original rank.

def Anderson4D.PartialPairing.wickRankIndex {n : ℕ} (κ : PartialPairing (Fin n)) (xt : Fin (n + 2) → T4) (j : Fin κ.singles.card) : Fin (wickAtSingleLabels κ xt).length

The rank j transported to the definitionally equal length of the Wick label list.

Equations

• κ.wickRankIndex xt j = Fin.cast ⋯ j

@[simp]

theorem Anderson4D.PartialPairing.wickRankIndex_val {n : ℕ} (κ : PartialPairing (Fin n)) (xt : Fin (n + 2) → T4) (j : Fin κ.singles.card) : ↑(κ.wickRankIndex xt j) = ↑j

theorem Anderson4D.PartialPairing.wickAtSingleLabels_get_wickRankIndex {n : ℕ} (κ : PartialPairing (Fin n)) (xt : Fin (n + 2) → T4) (j : Fin κ.singles.card) : (wickAtSingleLabels κ xt).get (κ.wickRankIndex xt j) = xt (varIdx ((κ.singles.orderEmbOfFin ⋯) j))

Looking up the Wick label at an increasing single rank returns the ambient variable at the corresponding ordered single index.

theorem Anderson4D.PartialPairing.diffFactor_hdSuccPair {n : ℕ} (xt : Fin (n + 3) → T4) (p : Fin n × Fin n) : diffFactor xt (hdSuccPair p) = diffFactor (ambientTailTuple ⋯ xt) p

A shifted extracted pair has exactly the old difference factor on the tuple with its first coordinate removed.

theorem Anderson4D.PartialPairing.chainProduct_wickHeadEquiv_contraction {n : ℕ} (d : MarkedSingle (Fin n)) (hExtract : ContractionExtractCompatible d) (xt : Fin (n + 3) → T4) : (∏ e : Fin (n + 2), if ↑e ∈ List.map (fun (p : Fin (n + 1) × Fin (n + 1)) => ↑p.2 + 1) (extract ((wickHeadEquiv n) (Sum.inr d))) then 1 else greenFn (xt e.castSucc - xt e.succ)) = greenFn (xt 0 - xt 1) * ∏ e : Fin (n + 1), if ↑e ∈ List.map (fun (p : Fin n × Fin n) => ↑p.2 + 1) (extract d.pairing) then 1 else greenFn (ambientTailTuple ⋯ xt e.castSucc - ambientTailTuple ⋯ xt e.succ)

Under extraction compatibility, adjoining the paired head adds only the new first Green edge to the chain product.

theorem Anderson4D.PartialPairing.differenceProduct_wickHeadEquiv_contraction {n : ℕ} (d : MarkedSingle (Fin n)) (hExtract : ContractionExtractCompatible d) (xt : Fin (n + 3) → T4) : (List.map (diffFactor xt) (extract ((wickHeadEquiv n) (Sum.inr d)))).prod = (List.map (diffFactor (ambientTailTuple ⋯ xt)) (extract d.pairing)).prod

Under extraction compatibility, the difference-factor product is the old product on the tail tuple.

theorem Anderson4D.PartialPairing.covarianceProduct_wickHeadEquiv_contraction (ρ : SmoothCutoff) (ε : ℝ) {n : ℕ} (d : MarkedSingle (Fin n)) (xt : Fin (n + 3) → T4) : ∏ k ∈ ((wickHeadEquiv n) (Sum.inr d)).pairSupport with k < ((wickHeadEquiv n) (Sum.inr d)) k, ρ.etaEpsT4 ε (xt (varIdx k) - xt (varIdx (((wickHeadEquiv n) (Sum.inr d)) k))) = ρ.etaEpsT4 ε (xt 1 - ambientTailTuple ⋯ xt (varIdx d.index)) * ∏ i ∈ d.pairing.pairSupport with i < d.pairing i, ρ.etaEpsT4 ε (ambientTailTuple ⋯ xt (varIdx i) - ambientTailTuple ⋯ xt (varIdx (d.pairing i)))

The covariance ledger of a contraction consists of the new head--partner covariance and the old covariance product.

theorem Anderson4D.PartialPairing.detIntegrand_wickHeadEquiv_contraction (ρ : SmoothCutoff) (ε : ℝ) {n : ℕ} (d : MarkedSingle (Fin n)) (hExtract : ContractionExtractCompatible d) (xt : Fin (n + 3) → T4) : detIntegrand ρ ε (n + 1) ((wickHeadEquiv n) (Sum.inr d)) xt = greenFn (xt 0 - xt 1) * (ρ.etaEpsT4 ε (xt 1 - ambientTailTuple ⋯ xt (varIdx d.index)) * detIntegrand ρ ε n d.pairing (ambientTailTuple ⋯ xt))

Deterministic closed-form factorization for a paired head whose extraction list only shifts under head deletion.

theorem Anderson4D.PartialPairing.wickAt_wickHeadEquiv_contraction (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) {n : ℕ} (d : MarkedSingle (Fin n)) (xt : Fin (n + 3) → T4) (ω : M.Ω) : wickAt M ρ ε ((wickHeadEquiv n) (Sum.inr d)) xt ω = wickPolynomial (fun (x y : T4) => ρ.etaEpsT4 ε (x - y)) (fun (x : T4) (ω' : M.Ω) => M.xiEps ρ ε ω' x) ((wickAtSingleLabels d.pairing (ambientTailTuple ⋯ xt)).eraseIdx (List.idxOf d.index (d.pairing.singles.sort fun (a b : Fin n) => a ≤ b))) ω

The Wick factor of a contraction is the Wick polynomial with the marked old single removed.

theorem Anderson4D.PartialPairing.headPairedContractionTerm_eq_randIntegrand (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) {n : ℕ} (d : MarkedSingle (Fin n)) (hExtract : ContractionExtractCompatible d) (xt : Fin (n + 3) → T4) (ω : M.Ω) : greenFn (xt 0 - xt 1) * (detIntegrand ρ ε n d.pairing (ambientTailTuple ⋯ xt) * (ρ.etaEpsT4 ε (xt 1 - ambientTailTuple ⋯ xt (varIdx d.index)) * wickPolynomial (fun (x y : T4) => ρ.etaEpsT4 ε (x - y)) (fun (x : T4) (ω' : M.Ω) => M.xiEps ρ ε ω' x) ((wickAtSingleLabels d.pairing (ambientTailTuple ⋯ xt)).eraseIdx (List.idxOf d.index (d.pairing.singles.sort fun (a b : Fin n) => a ≤ b))) ω)) = randIntegrand M ρ ε ((wickHeadEquiv n) (Sum.inr d)) xt ω

Pointwise Wick-contraction compatibility, conditional only on the explicit extraction shift that distinguishes paper case (2) from case (3).

noncomputable def Anderson4D.PartialPairing.headPairedContractionContribution (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (d : MarkedSingle (Fin n)) (x y : T4) (ω : M.Ω) : ℝ

The integrated contraction source attached to one marked old single. Its indexing is deliberately by MarkedSingle: the separate rank ledger below identifies this with the j-th term in the Wick recursion.

Equations

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

noncomputable def Anderson4D.PartialPairing.rankedContractionContribution (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (κ : PartialPairing (Fin n)) (j : Fin κ.singles.card) (x y : T4) (ω : M.Ω) : ℝ

The same contraction source in the rank indexing produced directly by the Wick creation--contraction formula.

Equations

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

theorem Anderson4D.PartialPairing.rankedContractionContribution_eq_headPaired (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (κ : PartialPairing (Fin n)) (j : Fin κ.singles.card) (x y : T4) (ω : M.Ω) : rankedContractionContribution M ρ lam ε n κ j x y ω = headPairedContractionContribution M ρ lam ε n ((rankedSingleEquiv (Fin n)) ⟨κ, j⟩) x y ω

Rank indexing and marked-single indexing define literally the same integrated contraction source.

theorem Anderson4D.PartialPairing.headPairedContractionContribution_eq_randRI (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (d : MarkedSingle (Fin n)) (hExtract : ContractionExtractCompatible d) (x y : T4) (ω : M.Ω) (hint : MeasureTheory.Integrable (fun (u : Fin (n + 1) → T4) => randIntegrand M ρ ε ((wickHeadEquiv n) (Sum.inr d)) (assemble x y u) ω) (MeasureTheory.Measure.pi fun (x : Fin (n + 1)) => paperMeasure)) : headPairedContractionContribution M ρ lam ε n d x y ω = randRI M ρ lam ε (n + 1) ((wickHeadEquiv n) (Sum.inr d)) x y ω

Integrated paired-head contraction. Under the exact extraction shift for paper case (2) and the Fubini integrability hypothesis, the contraction source is the random kernel indexed by the new pairing.

theorem Anderson4D.PartialPairing.rankedContractionContribution_eq_randRI (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (κ : PartialPairing (Fin n)) (j : Fin κ.singles.card) (hExtract : ContractionExtractCompatible ((rankedSingleEquiv (Fin n)) ⟨κ, j⟩)) (x y : T4) (ω : M.Ω) (hint : MeasureTheory.Integrable (fun (u : Fin (n + 1) → T4) => randIntegrand M ρ ε ((wickHeadEquiv n) (Sum.inr ((rankedSingleEquiv (Fin n)) ⟨κ, j⟩))) (assemble x y u) ω) (MeasureTheory.Measure.pi fun (x : Fin (n + 1)) => paperMeasure)) : rankedContractionContribution M ρ lam ε n κ j x y ω = randRI M ρ lam ε (n + 1) ((wickHeadEquiv n) (Sum.inr ((rankedSingleEquiv (Fin n)) ⟨κ, j⟩))) x y ω

The integrated contraction theorem in the rank indexing occurring in the Wick recursion.