The paper-facing left parametrix source

This module identifies the finite pairing sum used by the Wick creation--contraction analysis with the actual left-composition term

λ_ε ∫ G(x-z) ξ_ε(z) Pₙ(z,y) dz.

Only the exchange of the finite pairing sum with the outer integral needs an integrability hypothesis. Moving the scalar coupling factors through the totalized Bochner integrals is unconditional.

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

The left noise part of G (λ_ε ξ_ε - C_ε) Pₙ, in the notation of paper (3.17).

Equations

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

theorem Anderson4D.PartialPairing.leftNoisePairingContribution_eq_leftRandRI (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (κ : PartialPairing (Fin n)) (x y : T4) (ω : M.Ω) : leftNoisePairingContribution M ρ lam ε n κ x y ω = lamEps lam ε * ∫ (z : T4), greenFn (x - z) * (M.xiEps ρ ε ω z * randRI M ρ lam ε n κ z y ω) ∂paperMeasure

One pairing contribution is exactly the corresponding summand of the paper-facing left noise source. No integrability hypothesis is needed: scalar multiplication commutes with the totalized Bochner integral also on its junk branch.

structure Anderson4D.PartialPairing.LeftOrderSourceIntegrability (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (x y : T4) (ω : M.Ω) : Prop

Exact analytic input for exchanging the finite old-pairing sum with the outer spatial integral.

• pairing_outer (κ : PartialPairing (Fin n)) : MeasureTheory.Integrable (fun (z : T4) => greenFn (x - z) * (M.xiEps ρ ε ω z * randRI M ρ lam ε n κ z y ω)) paperMeasure

theorem Anderson4D.PartialPairing.leftNoiseOrderContribution_eq_leftParametrixNoiseSource (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (x y : T4) (ω : M.Ω) (hint : LeftOrderSourceIntegrability M ρ lam ε n x y ω) : leftNoiseOrderContribution M ρ lam ε n x y ω = leftParametrixNoiseSource M ρ lam ε n x y ω

The integrated pairing source used by the head-case analysis is the actual left noise term containing the order-n parametrix.