Orderwise symmetry of the random parametrix

The closed detIntegrand is deliberately right-oriented: an extracted interval replaces its right boundary edge. Consequently it is not pointwise invariant under chain reversal. This module instead uses the graded resolvent-word expansion forced by Proposition 3.4. Every word kernel is manifestly transposed by reversing the word and all integration coordinates; reversal is a bijection on compositions of the total order.

Graded resolvent words

noncomputable def Anderson4D.PartialPairing.renormWordWeight (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (d : ℕ) (z : T4) (ω : M.Ω) : ℝ

Vertex weight of a graded resolvent word. A block of size 1 is one mollified-noise insertion. A positive even block is a scalar counterterm insertion; all other block sizes carry zero weight.

Equations

• Anderson4D.PartialPairing.renormWordWeight M ρ lam ε d z ω = if d = 1 then Anderson4D.lamEps lam ε * M.xiEps ρ ε ω z else if Even d then -Anderson4D.renormC2q ρ lam ε (d / 2) else 0

noncomputable def Anderson4D.PartialPairing.renormWordIntegrandOnTuple (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (word : List ℕ) (xt : Fin (word.length + 2) → T4) (ω : M.Ω) : ℝ

A finite graded word evaluated on a full chain tuple.

Equations

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

noncomputable def Anderson4D.PartialPairing.renormWordKernel (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (word : List ℕ) (x y : T4) (ω : M.Ω) : ℝ

The spatial multiple integral attached to one graded word.

Equations

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

def Anderson4D.PartialPairing.renormWordReverseIndexEquiv (word : List ℕ) : Fin word.length ≃ Fin word.reverse.length

Reversal of a word's vertex indices, including the harmless cast between the propositionally equal list lengths.

Equations

• Anderson4D.PartialPairing.renormWordReverseIndexEquiv word = Equiv.trans Fin.revPerm (finCongr ⋯)

def Anderson4D.PartialPairing.renormWordReverseFullIndexEquiv (word : List ℕ) : Fin (word.length + 2) ≃ Fin (word.reverse.length + 2)

Reversal of the full chain slots.

Equations

• Anderson4D.PartialPairing.renormWordReverseFullIndexEquiv word = Equiv.trans Fin.revPerm (finCongr ⋯)

def Anderson4D.PartialPairing.renormWordReverseEdgeIndexEquiv (word : List ℕ) : Fin (word.length + 1) ≃ Fin (word.reverse.length + 1)

Reversal of chain-edge indices.

Equations

• Anderson4D.PartialPairing.renormWordReverseEdgeIndexEquiv word = Equiv.trans Fin.revPerm (finCongr ⋯)

@[simp]

theorem Anderson4D.PartialPairing.renormWordReverseIndexEquiv_val (word : List ℕ) (i : Fin word.length) : ↑((renormWordReverseIndexEquiv word) i) = word.length - 1 - ↑i

@[simp]

theorem Anderson4D.PartialPairing.renormWordReverseFullIndexEquiv_val (word : List ℕ) (i : Fin (word.length + 2)) : ↑((renormWordReverseFullIndexEquiv word) i) = word.length + 2 - 1 - ↑i

@[simp]

theorem Anderson4D.PartialPairing.renormWordReverseEdgeIndexEquiv_val (word : List ℕ) (i : Fin (word.length + 1)) : ↑((renormWordReverseEdgeIndexEquiv word) i) = word.length + 1 - 1 - ↑i

Measure-preserving reversal of the integration variables

noncomputable def Anderson4D.PartialPairing.renormWordReverseVariablesEquiv (word : List ℕ) : (Fin word.length → T4) ≃ᵐ (Fin word.reverse.length → T4)

Reverse the integration-variable coordinates of a graded word.

Equations

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

@[simp]

theorem Anderson4D.PartialPairing.renormWordReverseVariablesEquiv_apply (word : List ℕ) (v : Fin word.length → T4) (i : Fin word.length) : (renormWordReverseVariablesEquiv word) v ((renormWordReverseIndexEquiv word) i) = v i

theorem Anderson4D.PartialPairing.measurePreserving_renormWordReverseVariablesEquiv (word : List ℕ) : MeasureTheory.MeasurePreserving (⇑(renormWordReverseVariablesEquiv word)) (MeasureTheory.Measure.pi fun (x : Fin word.length) => paperMeasure) (MeasureTheory.Measure.pi fun (x : Fin word.reverse.length) => paperMeasure)

Coordinate reversal preserves the finite product of paper Haar measures.

theorem Anderson4D.PartialPairing.assemble_renormWordReverseVariablesEquiv (word : List ℕ) (x y : T4) (v : Fin word.length → T4) (i : Fin (word.length + 2)) : assemble y x ((renormWordReverseVariablesEquiv word) v) ((renormWordReverseFullIndexEquiv word) i) = assemble x y v i

Reversing all internal coordinates and swapping the two external points reverses the assembled full chain.

@[simp]

theorem Anderson4D.PartialPairing.reverse_get_renormWordReverseIndexEquiv (word : List ℕ) (i : Fin word.length) : word.reverse.get ((renormWordReverseIndexEquiv word) i) = word.get i

theorem Anderson4D.PartialPairing.assemble_reverseEdge_castSucc (word : List ℕ) (x y : T4) (v : Fin word.length → T4) (e : Fin (word.length + 1)) : assemble y x ((renormWordReverseVariablesEquiv word) v) ((renormWordReverseEdgeIndexEquiv word) e).castSucc = assemble x y v e.succ

The left endpoint of a reversed edge is the reversal of the original edge's right endpoint.

theorem Anderson4D.PartialPairing.assemble_reverseEdge_succ (word : List ℕ) (x y : T4) (v : Fin word.length → T4) (e : Fin (word.length + 1)) : assemble y x ((renormWordReverseVariablesEquiv word) v) ((renormWordReverseEdgeIndexEquiv word) e).succ = assemble x y v e.castSucc

The right endpoint of a reversed edge is the reversal of the original edge's left endpoint.

Pointwise symmetry of a graded word

theorem Anderson4D.PartialPairing.renormWordIntegrandOnTuple_reverse_assemble (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (word : List ℕ) (x y : T4) (v : Fin word.length → T4) (ω : M.Ω) : renormWordIntegrandOnTuple M ρ lam ε word.reverse (assemble y x ((renormWordReverseVariablesEquiv word) v)) ω = renormWordIntegrandOnTuple M ρ lam ε word (assemble x y v) ω

Reversing a word and all chain coordinates transposes its integrand.

theorem Anderson4D.PartialPairing.renormWordKernel_reverse (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (word : List ℕ) (x y : T4) (ω : M.Ω) : renormWordKernel M ρ lam ε word x y ω = renormWordKernel M ρ lam ε word.reverse y x ω

Every graded resolvent-word kernel is transposed by reversing the word. No integrability hypothesis is needed because the change of variables is measure preserving.

theorem Anderson4D.PartialPairing.renormWordKernel_nil (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (x y : T4) (ω : M.Ω) : renormWordKernel M ρ lam ε [] x y ω = greenFn (x - y)

The empty graded word is the free Green kernel.

Composition sum of all graded words

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

Sum of all graded resolvent words of total order n. Positivity of composition blocks excludes a spurious degree-zero vertex.

Equations

• Anderson4D.PartialPairing.gradedParametrix M ρ lam ε n x y ω = ∑ c : Composition n, Anderson4D.PartialPairing.renormWordKernel M ρ lam ε c.blocks x y ω

theorem Anderson4D.PartialPairing.gradedParametrix_symmetric (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (x y : T4) (ω : M.Ω) : gradedParametrix M ρ lam ε n x y ω = gradedParametrix M ρ lam ε n y x ω

The complete graded-word sum is symmetric: composition reversal is a bijection and transposes every individual word.

theorem Anderson4D.PartialPairing.gradedParametrix_zero (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (x y : T4) (ω : M.Ω) : gradedParametrix M ρ lam ε 0 x y ω = greenFn (x - y)

The order-zero graded sum is the free Green kernel.

Head decomposition of graded words

theorem Anderson4D.PartialPairing.integral_finSucc_zero {n : ℕ} (f : (Fin (n + 1) → T4) → ℝ) (hf : MeasureTheory.Integrable f (MeasureTheory.Measure.pi fun (x : Fin (n + 1)) => paperMeasure)) : (∫ (v : Fin (n + 1) → T4), f v ∂MeasureTheory.Measure.pi fun (x : Fin (n + 1)) => paperMeasure) = ∫ (z : T4), ∫ (v : Fin n → T4), f (Fin.cons z v) ∂MeasureTheory.Measure.pi fun (x : Fin n) => paperMeasure ∂paperMeasure

Fubini after separating the zero-th coordinate of a finite tuple. Only integrability of the original joint function is assumed; no pointwise integrability of the sections is required.

theorem Anderson4D.PartialPairing.integrable_integral_finSucc_zero {n : ℕ} (f : (Fin (n + 1) → T4) → ℝ) (hf : MeasureTheory.Integrable f (MeasureTheory.Measure.pi fun (x : Fin (n + 1)) => paperMeasure)) : MeasureTheory.Integrable (fun (z : T4) => ∫ (v : Fin n → T4), f (Fin.cons z v) ∂MeasureTheory.Measure.pi fun (x : Fin n) => paperMeasure) paperMeasure

The outer integral of the zero-th-coordinate sections is integrable whenever the original joint function is integrable.

theorem Anderson4D.PartialPairing.assemble_cons_succ (word : List ℕ) (x y z : T4) (v : Fin word.length → T4) (i : Fin (word.length + 2)) : assemble x y (Fin.cons z v) i.succ = assemble z y v i

Dropping the first variable from an assembled nonempty chain turns the old external left point into that first variable.

theorem Anderson4D.PartialPairing.renormWordIntegrandOnTuple_cons (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (d : ℕ) (word : List ℕ) (x y z : T4) (v : Fin word.length → T4) (ω : M.Ω) : renormWordIntegrandOnTuple M ρ lam ε (d :: word) (assemble x y (Fin.cons z v)) ω = greenFn (x - z) * renormWordWeight M ρ lam ε d z ω * renormWordIntegrandOnTuple M ρ lam ε word (assemble z y v) ω

A nonempty word integrand separates into its first edge, first vertex weight, and the remaining word integrand.

def Anderson4D.PartialPairing.RenormWordIntegrable (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (word : List ℕ) (x y : T4) (ω : M.Ω) : Prop

Joint integrability of one flat graded-word kernel. This is the right hypothesis for Fubini: section integrability is then needed only almost everywhere and is supplied by integral_prod.

Equations

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

theorem Anderson4D.PartialPairing.renormWordKernel_cons (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (d : ℕ) (word : List ℕ) (x y : T4) (ω : M.Ω) (hflat : RenormWordIntegrable M ρ lam ε (d :: word) x y ω) : renormWordKernel M ρ lam ε (d :: word) x y ω = ∫ (z : T4), greenFn (x - z) * renormWordWeight M ρ lam ε d z ω * renormWordKernel M ρ lam ε word z y ω ∂paperMeasure

A flat nonempty word kernel is its first weighted Green convolution with the remaining word kernel.

theorem Anderson4D.PartialPairing.integrable_renormWordHeadConvolution (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (d : ℕ) (word : List ℕ) (x y : T4) (ω : M.Ω) (hflat : RenormWordIntegrable M ρ lam ε (d :: word) x y ω) : MeasureTheory.Integrable (fun (z : T4) => greenFn (x - z) * renormWordWeight M ρ lam ε d z ω * renormWordKernel M ρ lam ε word z y ω) paperMeasure

Joint flat-word integrability implies integrability of the first weighted Green convolution with the tail kernel.

Compositions classified by their first block

def Anderson4D.PartialPairing.compositionHeadTail (n : ℕ) : Composition (n + 1) → (k : Fin (n + 1)) × Composition (n - ↑k)

Remove the positive first block from a composition of n+1. The finite index stores that block minus one.

Equations

• Anderson4D.PartialPairing.compositionHeadTail n { blocks := [], blocks_pos := blocks_pos, blocks_sum := hsum } = ⋯.elim
• Anderson4D.PartialPairing.compositionHeadTail n { blocks := 0 :: tail, blocks_pos := hpos, blocks_sum := blocks_sum } = ⋯.elim
• Anderson4D.PartialPairing.compositionHeadTail n { blocks := k.succ :: word, blocks_pos := hpos, blocks_sum := hsum } = ⟨⟨k, ⋯⟩, { blocks := word, blocks_pos := ⋯, blocks_sum := ⋯ }⟩

def Anderson4D.PartialPairing.compositionPrepend (n : ℕ) : (k : Fin (n + 1)) × Composition (n - ↑k) → Composition (n + 1)

Prepend the block k+1 to a composition of the remaining degree.

Equations

• Anderson4D.PartialPairing.compositionPrepend n ⟨k, c⟩ = { blocks := (↑k + 1) :: c.blocks, blocks_pos := ⋯, blocks_sum := ⋯ }

def Anderson4D.PartialPairing.compositionHeadEquiv (n : ℕ) : Composition (n + 1) ≃ (k : Fin (n + 1)) × Composition (n - ↑k)

Classifying a nonempty composition by its first block is a finite equivalence.

Equations

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

theorem Anderson4D.PartialPairing.gradedParametrix_succ_eq_sum_head (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (x y : T4) (ω : M.Ω) : gradedParametrix M ρ lam ε (n + 1) x y ω = ∑ k : Fin (n + 1), ∑ c : Composition (n - ↑k), renormWordKernel M ρ lam ε ((↑k + 1) :: c.blocks) x y ω

The order-n+1 graded sum, classified by the size of its first positive block.

theorem Anderson4D.PartialPairing.gradedParametrix_succ_eq_headConvolutions (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (x y : T4) (ω : M.Ω) (hflat : ∀ (k : Fin (n + 1)) (c : Composition (n - ↑k)), RenormWordIntegrable M ρ lam ε ((↑k + 1) :: c.blocks) x y ω) : gradedParametrix M ρ lam ε (n + 1) x y ω = ∑ k : Fin (n + 1), ∫ (z : T4), greenFn (x - z) * renormWordWeight M ρ lam ε (↑k + 1) z ω * gradedParametrix M ρ lam ε (n - ↑k) z y ω ∂paperMeasure

Head-block recurrence for the graded sum. Joint integrability is required only for the finitely many flat words at the new order.

Even head blocks

def Anderson4D.PartialPairing.evenHeadIndex (n : ℕ) (q : ↥(Finset.Icc 1 ((n + 1) / 2))) : { k : Fin (n + 1) // Even (↑k + 1) }

The even block of order 2q as a head index (block size minus one).

Equations

• Anderson4D.PartialPairing.evenHeadIndex n q = ⟨⟨2 * ↑q - 1, ⋯⟩, ⋯⟩

def Anderson4D.PartialPairing.evenHeadOrder (n : ℕ) (k : { k : Fin (n + 1) // Even (↑k + 1) }) : ↥(Finset.Icc 1 ((n + 1) / 2))

Recover q from an even positive head block 2q.

Equations

• Anderson4D.PartialPairing.evenHeadOrder n k = ⟨(↑↑k + 1) / 2, ⋯⟩

def Anderson4D.PartialPairing.evenHeadIndexEquiv (n : ℕ) : ↥(Finset.Icc 1 ((n + 1) / 2)) ≃ { k : Fin (n + 1) // Even (↑k + 1) }

Positive even head blocks are in bijection with the paper's counterterm range q ∈ [1, ⌊(n+1)/2⌋].

Equations

• Anderson4D.PartialPairing.evenHeadIndexEquiv n = { toFun := Anderson4D.PartialPairing.evenHeadIndex n, invFun := Anderson4D.PartialPairing.evenHeadOrder n, left_inv := ⋯, right_inv := ⋯ }

theorem Anderson4D.PartialPairing.headSelector_sum (n : ℕ) (A : ℝ) (B : ℕ → ℝ) : (∑ k : Fin (n + 1), if ↑k = 0 then A else if Even (↑k + 1) then -B ((↑k + 1) / 2) else 0) = A - ∑ q ∈ Finset.Icc 1 ((n + 1) / 2), B q

Summing a head-block selector leaves its degree-one term and the negative contributions of exactly the positive even blocks.

Proposition 3.4 recurrence for the graded sum

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

Degree-one head contribution for the graded parametrix.

Equations

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

noncomputable def Anderson4D.PartialPairing.gradedCountertermBlock (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (q r : ℕ) (x y : T4) (ω : M.Ω) : ℝ

Positive even head contribution for the graded parametrix.

Equations

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

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

Sum of the positive even graded head blocks at order n+1.

Equations

• Anderson4D.PartialPairing.gradedOrderCountertermSum M ρ lam ε n x y ω = ∑ q ∈ Finset.Icc 1 ((n + 1) / 2), Anderson4D.PartialPairing.gradedCountertermBlock M ρ lam ε q (n + 1 - 2 * q) x y ω

theorem Anderson4D.PartialPairing.gradedParametrix_succ_eq_noise_sub_counterterms (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (x y : T4) (ω : M.Ω) (hflat : ∀ (k : Fin (n + 1)) (c : Composition (n - ↑k)), RenormWordIntegrable M ρ lam ε ((↑k + 1) :: c.blocks) x y ω) : gradedParametrix M ρ lam ε (n + 1) x y ω = gradedParametrixNoiseSource M ρ lam ε n x y ω - gradedOrderCountertermSum M ρ lam ε n x y ω

The graded composition sum satisfies the left recurrence of Proposition 3.4.