The paper-facing right parametrix source

This is the right-composition analogue of IdentityLeftOperator. It expands

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

as a finite sum of pairing-level nested integrals, with the one finite-sum/integral exchange hypothesis stated explicitly.

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

The actual right-composition noise source for one old pairing.

Equations

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

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

One right pairing contribution is the corresponding summand of the paper-facing right source.

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

The full right noise source at old order n, before its Wick head-case split.

Equations

• Anderson4D.PartialPairing.rightNoiseOrderContribution M ρ lam ε n x y ω = ∑ κ : Anderson4D.PartialPairing (Fin n), Anderson4D.PartialPairing.rightNoisePairingContribution M ρ lam ε n κ x y ω

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

Exact analytic input for exchanging the finite old-pairing sum with the right source integral.

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

theorem Anderson4D.PartialPairing.rightNoiseOrderContribution_eq_rightParametrixNoiseSource (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (x y : T4) (ω : M.Ω) (hint : RightOrderSourceIntegrability M ρ lam ε n x y ω) : rightNoiseOrderContribution M ρ lam ε n x y ω = rightParametrixNoiseSource M ρ lam ε n x y ω

The integrated right pairing source is the actual right noise-composition term containing Pₙ.