Deterministic parametrix: renormalized kernels and constants

Paper: D-Kdet — (3.1)–(3.2) — deterministic profile kernels

Definition layer for the deterministic side of the parametrix expansion of Deng–Shen (arXiv:2607.10105): blueprint nodes D-Kdet (the closed-form renormalized integrand, paper (3.6)), D-RI closed form (the kernels detRIfull/detRIprofile and the J kernels, paper (3.12)) and D-C2q (the renormalization constants, paper (3.10)–(3.11)). All paper indices 1..m are shifted down by one (0-based Fin indices); the external points x = x_0, y = x_{m+1} occupy the two extra slots of assemble.

Junk-totalization (DESIGN §5.7)

Every analytic definition below is total:

• tsum and Bochner integrals default to 0 off summability/integrability;
• index-overflow branches (which the good combinatorial class never hits) produce the factor 1 via dite;
• detJ at q = 0 is 0. The analytic estimates carry the hypotheses excluding the junk branches.

noncomputable def Anderson4D.SmoothCutoff.etaEpsT4 (ρ : SmoothCutoff) (ε : ℝ) (z : T4) : ℝ

The periodized mollified covariance η_ε on the torus: η_ε(x) = ε⁻⁴ η(x/ε) with η = ρ ⋆ ρ (SmoothCutoff.eta), periodized over the lattice 2πℤ⁴ through the canonical lift. The tsum is junk-totalized: it is 0 if the family is not summable; genuine cutoffs give a finite sum.

Equations

• ρ.etaEpsT4 ε z = ∑' (k : Anderson4D.Z4), ε⁻¹ ^ Anderson4D.dim * ρ.eta fun (i : Fin Anderson4D.dim) => ε⁻¹ * (Anderson4D.torusLift z i + 2 * Real.pi * ↑(k i))

def Anderson4D.varIdx {m : ℕ} (i : Fin m) : Fin (m + 2)

The slot of the i-th integration variable inside the assembled (m+2)-tuple: paper variable x_{i+1} (0-based shift).

Equations

• Anderson4D.varIdx i = ⟨↑i + 1, ⋯⟩

@[simp]

theorem Anderson4D.varIdx_val {m : ℕ} (i : Fin m) : ↑(varIdx i) = ↑i + 1

def Anderson4D.assemble {m : ℕ} (x y : T4) (v : Fin m → T4) : Fin (m + 2) → T4

Assemble the external points x, y and the m integration variables v into the full (m+2)-tuple (x, v_0, …, v_{m-1}, y): slot 0 is x, slot m+1 is y, slot j (for 1 ≤ j ≤ m) is v (j-1).

Equations

• Anderson4D.assemble x y v j = if _h0 : ↑j = 0 then x else if _hm : ↑j = m + 1 then y else v ⟨↑j - 1, ⋯⟩

@[simp]

theorem Anderson4D.assemble_zero {m : ℕ} (x y : T4) (v : Fin m → T4) : assemble x y v 0 = x

@[simp]

theorem Anderson4D.assemble_last {m : ℕ} (x y : T4) (v : Fin m → T4) : assemble x y v (Fin.last (m + 1)) = y

@[simp]

theorem Anderson4D.assemble_varIdx {m : ℕ} (x y : T4) (v : Fin m → T4) (i : Fin m) : assemble x y v (varIdx i) = v i

The renormalized integrand (paper (3.6), node D-Kdet)

noncomputable def Anderson4D.diffFactor {m : ℕ} (xt : Fin (m + 2) → T4) (p : Fin m × Fin m) : ℝ

Difference factor of the closed form (3.6) attached to an extracted pair p = (l, r) (0-based): G(x_{r+1} - x_{r+2}) - G(x_{l+1} - x_{r+2}) in assembled-slot indices (varIdx shifts by one; the slot r+2 is always in range since r < m). No junk branch is needed here.

Equations

• Anderson4D.diffFactor xt p = Anderson4D.greenFn (xt (Anderson4D.varIdx p.2) - xt ⟨↑p.2 + 2, ⋯⟩) - Anderson4D.greenFn (xt (Anderson4D.varIdx p.1) - xt ⟨↑p.2 + 2, ⋯⟩)

noncomputable def Anderson4D.detIntegrand (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (κ : PartialPairing (Fin m)) (xt : Fin (m + 2) → T4) : ℝ

Closed form of the renormalized integrand (paper (3.6), 0-based; node D-Kdet), evaluated on the assembled tuple xt = (x, v_0, …, v_{m-1}, y) : Fin (m+2) → T4:

• chain part: over each edge e : Fin (m+1) the factor G(xt e - xt (e+1)), excluded (replaced by 1) precisely when e = r + 1 for some extracted pair (l, r) ∈ extract κ — the paper replaces that chain factor by the difference factor;
• difference part: the product of diffFactor over extract κ;
• covariance part: η_ε(xt (i+1) - xt (κ i + 1)) over the pairs of κ (each pair counted once via its smaller endpoint).

Total by construction (greenFn, etaEpsT4 are junk-totalized).

Equations

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

The renormalized kernels (node D-RI closed form)

noncomputable def Anderson4D.detRIfull (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (κ : PartialPairing (Fin m)) (x y : T4) : ℝ

Fully integrated renormalized kernel (R^I λ_ε ξ_ε)-type value (paper (3.6) with all m internal variables integrated against paperMeasure^{⊗m}): the deterministic value of the order-m term for fully paired κ, and the total-integral form of the profile. The Bochner integral is junk-totalized (0 off integrability).

Equations

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

noncomputable def Anderson4D.detRIprofile (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (κ : PartialPairing (Fin m)) (x y : T4) (z : Fin m → T4) : ℝ

Profile kernel with singles free (feeds the random layer): only the paired variables (indices in κ.pairSupport) are integrated; the single-index values are supplied by z (only the values of z on the singles of κ matter). Junk-totalized Bochner integral.

Equations

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

The J kernels (paper (3.12), node D-C2q input)

noncomputable def Anderson4D.diffFactorJ {n : ℕ} (xtJ : Fin n → T4) (p : Fin n × Fin n) : ℝ

Difference factor of the J closed form (3.12) attached to an extracted pair p = (l, r) of a pairing of the full tuple (no external slots): G(xtJ r - xtJ (r+1)) - G(xtJ l - xtJ (r+1)). Junk branch: if r + 1 overflows (r is the last index — never the case on the good combinatorial class), the factor is 1.

Equations

• Anderson4D.diffFactorJ xtJ p = if h : ↑p.2 + 1 < n then Anderson4D.greenFn (xtJ p.2 - xtJ ⟨↑p.2 + 1, h⟩) - Anderson4D.greenFn (xtJ p.1 - xtJ ⟨↑p.2 + 1, h⟩) else 1

noncomputable def Anderson4D.detJintegrand (ρ : SmoothCutoff) (ε : ℝ) (q : ℕ) (σ : PartialPairing (Fin (2 * q))) (xtJ : Fin (2 * q) → T4) : ℝ

Closed form of the J integrand (paper (3.12), 0-based): the tuple xtJ : Fin (2q) → T4 is the paper tuple (x_1, …, x_{2q}). Chain factors G(xtJ e - xtJ (e+1)) over e : Fin (2q-1), excluded (replaced by 1) precisely when e = r for some (l, r) ∈ extract σ (paper: the chain factor with left paper-index r_i is replaced by the difference factor); then the diffFactorJ product and the covariance product over the pairs of σ. The chain indexing is guarded by a dite (junk factor 1) so that the formula is total also at q = 0; the guard e.val + 1 < 2q always holds for e : Fin (2q - 1).

Equations

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

noncomputable def Anderson4D.detJ (ρ : SmoothCutoff) (lam ε : ℝ) (q : ℕ) : PartialPairing (Fin (2 * q)) → T4 → T4 → ℝ

The kernel J_{2q,σ} (paper (3.12)): first and last of the 2q variables fixed at z and w, the internal 2q - 2 integrated against paperMeasure^{⊗(2q-2)}; the assembled tuple assemble z w v (of length (2q-2)+2 = 2q) is reindexed to Fin (2q) by Fin.cast. Junk value 0 at q = 0 (the paper only uses q ≥ 1); the Bochner integral is junk-totalized.

Equations

• One or more equations did not get rendered due to their size.
• Anderson4D.detJ ρ lam ε 0 x_4 x✝¹ x✝ = 0

def Anderson4D.IsNonSplit {q : ℕ} (σ : PartialPairing (Fin (2 * q))) : Prop

The non-concatenation class of paper §3.2: σ is full and no proper prefix {i : Fin (2q) | i ≤ p} (with p + 1 < 2q) is fully paired — equivalently (given fullness) σ does not split into two pairings of complementary prefixes. Stated with the bounded existential over p ∈ Finset.range (2q) (no loss: p + 1 < 2q forces p < 2q), which makes the predicate decidable.

Equations

• Anderson4D.IsNonSplit σ = (σ.IsFull ∧ ¬∃ p ∈ Finset.range (2 * q), p + 1 < 2 * q ∧ Anderson4D.IsFullyPairedOn σ {i : Fin (2 * q) | ↑i ≤ p})

@[implicit_reducible]

instance Anderson4D.instDecidableIsNonSplit {q : ℕ} (σ : PartialPairing (Fin (2 * q))) : Decidable (IsNonSplit σ)

Equations

• Anderson4D.instDecidableIsNonSplit σ = decidable_of_iff (σ.IsFull ∧ ¬∃ p ∈ Finset.range (2 * q), p + 1 < 2 * q ∧ Anderson4D.IsFullyPairedOn σ {i : Fin (2 * q) | ↑i ≤ p}) ⋯

The renormalization constants (paper (3.10)–(3.11), node D-C2q)

noncomputable def Anderson4D.renormC2q (ρ : SmoothCutoff) (lam ε : ℝ) (q : ℕ) : ℝ

The order-2q renormalization constant (paper (3.10)): the sum over the non-concatenation class of full pairings σ of Fin (2q) of the total integral of J_{2q,σ}(z, 0) in z (translation invariance makes fixing the second argument at 0 harmless — an M-layer lemma, not part of this definition). Junk-totalized integral.

Equations

• Anderson4D.renormC2q ρ lam ε q = ∑ σ : Anderson4D.PartialPairing (Fin (2 * q)) with Anderson4D.IsNonSplit σ, ∫ (z : Anderson4D.T4), Anderson4D.detJ ρ lam ε q σ z 0 ∂Anderson4D.paperMeasure

noncomputable def Anderson4D.renormCEps (ρ : SmoothCutoff) (lam ε : ℝ) : ℝ

The renormalization constant C_ε (paper (3.11)): the sum of renormC2q over 1 ≤ q ≤ A = truncOrder ε = ⌊|log ε|⌋.

Equations

• Anderson4D.renormCEps ρ lam ε = ∑ q ∈ Finset.Icc 1 (Anderson4D.truncOrder ε), Anderson4D.renormC2q ρ lam ε q

Sanity: the m = 0 kernel is the free Green's function

theorem Anderson4D.detRIfull_zero (ρ : SmoothCutoff) (lam ε : ℝ) (κ : PartialPairing (Fin 0)) (x y : T4) : detRIfull ρ lam ε 0 κ x y = greenFn (x - y)

Sanity check on the closed form: at order m = 0 there are no integration variables and no pairs (extract κ = []), the chain is the single edge x → y, and the empty product measure is the Dirac probability measure, so detRIfull collapses to G(x - y).