Parametrix identities

This file develops the analytic and finite-sum bridges used in Proposition 3.4, paper (3.16)--(3.17). The first section isolates the measure-preserving reindexing of a finite tuple into two consecutive blocks. This is the Fubini mechanism needed to separate the internal J variables from the variables of the remaining random kernel.

theorem Anderson4D.instIsFiniteMeasureT4PaperMeasure_1 : MeasureTheory.IsFiniteMeasure paperMeasure

Consecutive finite blocks and product measure

def Anderson4D.finAddPiMeasurableEquiv (a b : ℕ) (X : Type u_1) [MeasurableSpace X] : (Fin (a + b) → X) ≃ᵐ (Fin a → X) × (Fin b → X)

Reindex a tuple of length a + b as two consecutive tuples.

Equations

• Anderson4D.finAddPiMeasurableEquiv a b X = (MeasurableEquiv.piCongrLeft (fun (x : Fin (a + b)) => X) finSumFinEquiv).symm.trans (MeasurableEquiv.sumPiEquivProdPi fun (x : Fin a ⊕ Fin b) => X)

@[simp]

theorem Anderson4D.finAddPiMeasurableEquiv_apply (a b : ℕ) (X : Type u_1) [MeasurableSpace X] (v : Fin (a + b) → X) : (finAddPiMeasurableEquiv a b X) v = (fun (i : Fin a) => v (Fin.castAdd b i), fun (j : Fin b) => v (Fin.natAdd a j))

@[simp]

theorem Anderson4D.finAddPiMeasurableEquiv_symm_apply (a b : ℕ) (X : Type u_1) [MeasurableSpace X] (u : Fin a → X) (v : Fin b → X) : (finAddPiMeasurableEquiv a b X).symm (u, v) = Fin.append u v

theorem Anderson4D.measurePreserving_finAddPi (a b : ℕ) : MeasureTheory.MeasurePreserving (⇑(finAddPiMeasurableEquiv a b T4)) (MeasureTheory.Measure.pi fun (x : Fin (a + b)) => paperMeasure) ((MeasureTheory.Measure.pi fun (x : Fin a) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : Fin b) => paperMeasure))

Product Haar measure is preserved when a finite tuple is split into two consecutive blocks.

theorem Anderson4D.integral_finAdd {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (a b : ℕ) (f : (Fin (a + b) → T4) → E) (hf : MeasureTheory.Integrable f (MeasureTheory.Measure.pi fun (x : Fin (a + b)) => paperMeasure)) : (∫ (x : Fin (a + b) → T4), f x ∂MeasureTheory.Measure.pi fun (x : Fin (a + b)) => paperMeasure) = ∫ (u : Fin a → T4), ∫ (v : Fin b → T4), f (Fin.append u v) ∂MeasureTheory.Measure.pi fun (x : Fin b) => paperMeasure ∂MeasureTheory.Measure.pi fun (x : Fin a) => paperMeasure

Fubini after the concrete Fin (a+b) consecutive-block reindexing.

theorem Anderson4D.integral_finAdd_mul (a b : ℕ) (f : (Fin a → T4) → ℝ) (g : (Fin b → T4) → ℝ) : (∫ (x : Fin (a + b) → T4), (f fun (i : Fin a) => x (Fin.castAdd b i)) * g fun (j : Fin b) => x (Fin.natAdd a j) ∂MeasureTheory.Measure.pi fun (x : Fin (a + b)) => paperMeasure) = (∫ (u : Fin a → T4), f u ∂MeasureTheory.Measure.pi fun (x : Fin a) => paperMeasure) * ∫ (v : Fin b → T4), g v ∂MeasureTheory.Measure.pi fun (x : Fin b) => paperMeasure

A separated integrand factors after splitting consecutive finite blocks. integral_prod_mul makes this identity valid for totalized Bochner integrals without auxiliary integrability assumptions.

The analytic case-(3) block

def Anderson4D.detJTupleSucc (q : ℕ) (z w : T4) (u : Fin (2 * q) → T4) : Fin (2 * (q + 1)) → T4

Tuple (z,u,w) used by the positive-order J kernel. The arithmetic cast is the one appearing definitionally in detJ.

Equations

• Anderson4D.detJTupleSucc q z w u j = Anderson4D.assemble z w u (Fin.cast ⋯ j)

@[simp]

theorem Anderson4D.detJTupleSucc_zero (q : ℕ) (z w : T4) (u : Fin (2 * q) → T4) : detJTupleSucc q z w u 0 = z

noncomputable def Anderson4D.caseThreeJointCore (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (q r : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (τ : PartialPairing (Fin r)) (z w y : T4) (ω : M.Ω) (t : Fin (2 * q + r) → T4) : ℝ

The inner spatial integral of a case-(3) contribution before it is split into the fully paired prefix and the external remainder. The first 2q coordinates are the internal coordinates of J_{2(q+1)}; the last r coordinates belong to the remaining random kernel.

Equations

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

theorem Anderson4D.integral_caseThreeJointCore_eq_mul (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (q r : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (τ : PartialPairing (Fin r)) (z w y : T4) (ω : M.Ω) : (∫ (t : Fin (2 * q + r) → T4), caseThreeJointCore M ρ ε q r σ τ z w y ω t ∂MeasureTheory.Measure.pi fun (x : Fin (2 * q + r)) => paperMeasure) = (∫ (u : Fin (2 * q) → T4), detJintegrand ρ ε (q + 1) σ (detJTupleSucc q z w u) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * q)) => paperMeasure) * ∫ (v : Fin r → T4), randIntegrand M ρ ε τ (assemble w y v) ω ∂MeasureTheory.Measure.pi fun (x : Fin r) => paperMeasure

Exact finite-product Fubini factorization of the inner case-(3) integral. No analytic side condition is needed: after reindexing, the integrand is a separated product, so mathlib's totalized integral_prod_mul applies directly.

noncomputable def Anderson4D.caseThreeJointContribution (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (q r : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (τ : PartialPairing (Fin r)) (x y : T4) (ω : M.Ω) : ℝ

The unsplit case-(3) contribution, with the two boundary variables z,w kept outside and all other variables integrated in their ambient order.

Equations

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

noncomputable def Anderson4D.caseThreeFactorizedContribution (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (q r : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (τ : PartialPairing (Fin r)) (x y : T4) (ω : M.Ω) : ℝ

The paper (3.18) form of the same contribution: an internal J_{2(q+1),σ} multiplied by the external random kernel.

Equations

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

theorem Anderson4D.caseThreeJointContribution_eq_factorized (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (q r : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (τ : PartialPairing (Fin r)) (x y : T4) (ω : M.Ω) : caseThreeJointContribution M ρ lam ε q r σ τ x y ω = caseThreeFactorizedContribution M ρ lam ε q r σ τ x y ω

Case-(3) analytic bridge (paper (3.18)). Consecutive-variable reindexing, finite-product Fubini, and the coupling-power ledger turn the joint integral into detJ × randRI.

The right-composition analogue (paper (3.17))

noncomputable def Anderson4D.caseThreeRightJointCore (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (q r : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (τ : PartialPairing (Fin r)) (x z w : T4) (ω : M.Ω) (t : Fin (r + 2 * q) → T4) : ℝ

Mirrored case-(3) inner integrand: the external random block precedes the fully paired J block.

Equations

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

theorem Anderson4D.integral_caseThreeRightJointCore_eq_mul (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (q r : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (τ : PartialPairing (Fin r)) (x z w : T4) (ω : M.Ω) : (∫ (t : Fin (r + 2 * q) → T4), caseThreeRightJointCore M ρ ε q r σ τ x z w ω t ∂MeasureTheory.Measure.pi fun (x : Fin (r + 2 * q)) => paperMeasure) = (∫ (v : Fin r → T4), randIntegrand M ρ ε τ (assemble x z v) ω ∂MeasureTheory.Measure.pi fun (x : Fin r) => paperMeasure) * ∫ (u : Fin (2 * q) → T4), detJintegrand ρ ε (q + 1) σ (detJTupleSucc q z w u) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * q)) => paperMeasure

Fubini factorization for the right-composition case-(3) block.

noncomputable def Anderson4D.caseThreeRightJointContribution (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (q r : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (τ : PartialPairing (Fin r)) (x y : T4) (ω : M.Ω) : ℝ

The joint right-composition case-(3) contribution before separating the random and deterministic blocks.

Equations

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

noncomputable def Anderson4D.caseThreeRightFactorizedContribution (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (q r : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (τ : PartialPairing (Fin r)) (x y : T4) (ω : M.Ω) : ℝ

The factorized right-composition form, dual to paper (3.18).

Equations

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

theorem Anderson4D.caseThreeRightJointContribution_eq_factorized (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (q r : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (τ : PartialPairing (Fin r)) (x y : T4) (ω : M.Ω) : caseThreeRightJointContribution M ρ lam ε q r σ τ x y ω = caseThreeRightFactorizedContribution M ρ lam ε q r σ τ x y ω

Right case-(3) analytic bridge (paper (3.17)).

Finite sums of the counterterm block

noncomputable def Anderson4D.detJMass (ρ : SmoothCutoff) (lam ε : ℝ) (q : ℕ) (σ : PartialPairing (Fin (2 * q))) : ℝ

The scalar mass attached to one admissible internal pairing.

Equations

• Anderson4D.detJMass ρ lam ε q σ = ∫ (z : Anderson4D.T4), Anderson4D.detJ ρ lam ε q σ z 0 ∂Anderson4D.paperMeasure

theorem Anderson4D.sum_detJMass_mul_randRI (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (q r : ℕ) (x y : T4) (ω : M.Ω) : ∑ σ : PartialPairing (Fin (2 * q)) with IsNonSplit σ, ∑ τ : PartialPairing (Fin r), detJMass ρ lam ε q σ * randRI M ρ lam ε r τ x y ω = renormC2q ρ lam ε q * parametrixP M ρ lam ε r x y ω

The finite double sum over an internal non-split pairing and an arbitrary external pairing factors exactly into C₂q · Pᵣ. This is the finite-sum exchange in the delta part of paper (3.19).

theorem Anderson4D.sum_internal_external_mul {R : Type u_1} [CommSemiring R] {A : Type u_2} {B : Type u_3} [Fintype A] [Fintype B] (internal : A → R) (external : B → R) : ∑ a : A, ∑ b : B, internal a * external b = (∑ a : A, internal a) * ∑ b : B, external b

The same counterterm ledger with any external family in an arbitrary commutative semiring. It is useful when the external kernels have already been mapped to Fourier multipliers.

Translation ledger for J

theorem Anderson4D.assemble_add_const {n : ℕ} (x y a : T4) (v : Fin n → T4) (j : Fin (n + 2)) : assemble (x + a) (y + a) (fun (i : Fin n) => v i + a) j = assemble x y v j + a

theorem Anderson4D.detJintegrand_add_const (ρ : SmoothCutoff) (ε : ℝ) (q : ℕ) (σ : PartialPairing (Fin (2 * q))) (xt : Fin (2 * q) → T4) (a : T4) : (detJintegrand ρ ε q σ fun (i : Fin (2 * q)) => xt i + a) = detJintegrand ρ ε q σ xt

The closed J integrand only contains differences, hence a common translation of every spatial variable cancels pointwise.

theorem Anderson4D.detJ_add_const (ρ : SmoothCutoff) (lam ε : ℝ) (q : ℕ) (σ : PartialPairing (Fin (2 * q))) (z w a : T4) : detJ ρ lam ε q σ (z + a) (w + a) = detJ ρ lam ε q σ z w

Simultaneously translating both endpoints leaves the J kernel unchanged. The proof reindexes every internal coordinate by the same Haar translation.

theorem Anderson4D.detJ_eq_diff (ρ : SmoothCutoff) (lam ε : ℝ) (q : ℕ) (σ : PartialPairing (Fin (2 * q))) (z w : T4) : detJ ρ lam ε q σ z w = detJ ρ lam ε q σ (z - w) 0

Difference form of translation invariance.

noncomputable def Anderson4D.subLeftT4MeasurableEquiv (z : T4) : T4 ≃ᵐ T4

The coordinatewise involution w ↦ z - w, bundled as a measurable equivalence of the four-torus.

Equations

• Anderson4D.subLeftT4MeasurableEquiv z = MeasurableEquiv.piCongrRight fun (i : Fin Anderson4D.dim) => (MeasurableEquiv.neg (AddCircle (2 * Real.pi))).trans (MeasurableEquiv.addLeft (z i))

@[simp]

theorem Anderson4D.subLeftT4MeasurableEquiv_apply (z w : T4) : (subLeftT4MeasurableEquiv z) w = z - w

theorem Anderson4D.measurePreserving_subLeftT4 (z : T4) : MeasureTheory.MeasurePreserving (⇑(subLeftT4MeasurableEquiv z)) paperMeasure paperMeasure

Haar measure on the paper torus is invariant under w ↦ z - w.

theorem Anderson4D.integral_detJ_right_eq_mass (ρ : SmoothCutoff) (lam ε : ℝ) (q : ℕ) (σ : PartialPairing (Fin (2 * q))) (z : T4) : ∫ (w : T4), detJ ρ lam ε q σ z w ∂paperMeasure = detJMass ρ lam ε q σ

The mass of w ↦ J(z,w) is independent of z and equals the normalization used in renormC2q.

The delta/counterterm part of case (3)

noncomputable def Anderson4D.caseThreeDeltaContribution (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (q r : ℕ) (σ : PartialPairing (Fin (2 * q))) (τ : PartialPairing (Fin r)) (x y : T4) (ω : M.Ω) : ℝ

The second term in paper (3.19), after the formal delta distribution has collapsed w to z, but before replacing the mass of J by its translation-independent normalization.

Equations

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

theorem Anderson4D.caseThreeDeltaContribution_eq_mass (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (q r : ℕ) (σ : PartialPairing (Fin (2 * q))) (τ : PartialPairing (Fin r)) (x y : T4) (ω : M.Ω) : caseThreeDeltaContribution M ρ lam ε q r σ τ x y ω = ∫ (z : T4), greenFn (x - z) * detJMass ρ lam ε q σ * randRI M ρ lam ε r τ z y ω ∂paperMeasure

Translation invariance turns the collapsed J factor in (3.19) into the scalar mass used in the definition of C₂q.

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

The canonical finite double sum of all case-(3) counterterms at orders (2q,r), kept inside the outer Green convolution. Keeping the finite sum inside the integrand avoids imposing irrelevant integrability hypotheses merely to exchange a totalized Bochner integral and a sum.

Equations

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

theorem Anderson4D.caseThreeCountertermBlock_eq (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (q r : ℕ) (x y : T4) (ω : M.Ω) : caseThreeCountertermBlock M ρ lam ε q r x y ω = renormC2q ρ lam ε q * ∫ (z : T4), greenFn (x - z) * parametrixP M ρ lam ε r z y ω ∂paperMeasure

Counterterm collapse (paper (3.19)). The internal non-split pairing sum and the external pairing sum collapse pointwise to C₂q · Pᵣ under the outer Green convolution.

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

Right-composition counterpart of caseThreeCountertermBlock: after the delta collapse, Pᵣ lies to the left of the free Green kernel.

Equations

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

theorem Anderson4D.caseThreeRightCountertermBlock_eq (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (q r : ℕ) (x y : T4) (ω : M.Ω) : caseThreeRightCountertermBlock M ρ lam ε q r x y ω = renormC2q ρ lam ε q * ∫ (z : T4), parametrixP M ρ lam ε r x z ω * greenFn (z - y) ∂paperMeasure

Right counterterm collapse used in paper (3.17).

Pointwise creation--contraction for the random integrand

theorem Anderson4D.xi_mul_randIntegrand_eq_create_add_contract (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (κ : PartialPairing (Fin m)) (xt : Fin (m + 2) → T4) (z : T4) (ω : M.Ω) : M.xiEps ρ ε ω z * randIntegrand M ρ ε κ xt ω = detIntegrand ρ ε m κ xt * wickPolynomial (fun (x y : T4) => ρ.etaEpsT4 ε (x - y)) (fun (x : T4) (ω' : M.Ω) => M.xiEps ρ ε ω' x) (z :: wickAtSingleLabels κ xt) ω + ∑ j : Fin (wickAtSingleLabels κ xt).length, detIntegrand ρ ε m κ xt * (ρ.etaEpsT4 ε (z - (wickAtSingleLabels κ xt).get j) * wickPolynomial (fun (x y : T4) => ρ.etaEpsT4 ε (x - y)) (fun (x : T4) (ω' : M.Ω) => M.xiEps ρ ε ω' x) ((wickAtSingleLabels κ xt).eraseIdx ↑j) ω)

The Wick creation--contraction identity with the deterministic renormalized integrand carried through unchanged. This is the pointwise algebra at the start of the left-composition proof of (3.16), before the pairing reindexing into the three head cases.

The order-zero boundary term

theorem Anderson4D.wickAt_zero (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (κ : PartialPairing (Fin 0)) (xt : Fin (0 + 2) → T4) (ω : M.Ω) : wickAt M ρ ε κ xt ω = 1

At order zero the pairing has no single labels, so its Wick factor is the empty Wick polynomial.

theorem Anderson4D.randRI_zero (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (κ : PartialPairing (Fin 0)) (x y : T4) (ω : M.Ω) : randRI M ρ lam ε 0 κ x y ω = greenFn (x - y)

The random order-zero kernel is the free Green kernel.

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

The order-zero parametrix piece is exactly G; this is the left boundary term in the telescoping derivation of (3.20).