Finite-pairing expansion of parametrix coefficients

The pointwise identity parametrixP = ∑ κ, randRI κ only becomes an identity after the two external Bochner integrals once each summand is integrable in the corresponding nested order. This file records exactly that minimal spatial condition and proves the finite-sum and expectation algebra above it. No singular-integral estimate is assumed implicitly.

noncomputable def Anderson4D.pmPairingFourierIntegrand (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (α β : Z4) (κ : PartialPairing (Fin m)) (ω : M.Ω) (x y : T4) : ℂ

The Fourier integrand belonging to one within-copy partial pairing.

Equations

• Anderson4D.pmPairingFourierIntegrand M ρ lam ε m α β κ ω x y = Anderson4D.charT4 α x * Anderson4D.charT4 β y * ↑(Anderson4D.randRI M ρ lam ε m κ x y ω)

structure Anderson4D.PairingCoefficientSpatialIntegrable (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (α β : Z4) : Prop

Minimal joint spatial hypothesis needed to move the finite pairing sum through the two external integrals defining pmCoeff.

The product-space formulation is essential: it yields integrable sections almost everywhere by Fubini without incorrectly requiring every fixed Green-diagonal section to be integrable.

• joint (κ : PartialPairing (Fin m)) : ∀ᵐ (ω : M.Ω), MeasureTheory.Integrable (fun (p : T4 × T4) => pmPairingFourierIntegrand M ρ lam ε m α β κ ω p.1 p.2) (paperMeasure.prod paperMeasure)

theorem Anderson4D.pmPairingCoeff_eq_integral (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (α β : Z4) (κ : PartialPairing (Fin m)) (ω : M.Ω) : pmPairingCoeff M ρ lam ε m α β κ ω = ∫ (x : T4), ∫ (y : T4), pmPairingFourierIntegrand M ρ lam ε m α β κ ω x y ∂paperMeasure ∂paperMeasure

One pairing coefficient is the nested integral of its named Fourier integrand.

theorem Anderson4D.pmCoeff_eq_sum_pmPairingCoeff {M : NoiseModel} {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {α β : Z4} (hspatial : PairingCoefficientSpatialIntegrable M ρ lam ε m α β) : pmCoeff M ρ lam ε m α β =ᵐ[MeasureTheory.volume] fun (ω : M.Ω) => ∑ κ : PartialPairing (Fin m), pmPairingCoeff M ρ lam ε m α β κ ω

The coefficient of the finite pairing sum is the finite sum of the individual pairing coefficients.

theorem Anderson4D.memLp_pmPairingCoeff_of_pairingProduct_integrable {M : NoiseModel} {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {α β : Z4} (hprod : ∀ (κp κm : PartialPairing (Fin m)), MeasureTheory.Integrable (fun (ω : M.Ω) => pmPairingCoeff M ρ lam ε m α β κp ω * (starRingEnd ℂ) (pmPairingCoeff M ρ lam ε m α β κm ω)) MeasureTheory.volume) (κ : PartialPairing (Fin m)) : MeasureTheory.MemLp (pmPairingCoeff M ρ lam ε m α β κ) 2 MeasureTheory.volume

Diagonal pairing-product integrability gives L² membership of one pairing coefficient.

theorem Anderson4D.memLp_pmCoeff_of_pairingProduct_integrable {M : NoiseModel} {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {α β : Z4} (hspatial : PairingCoefficientSpatialIntegrable M ρ lam ε m α β) (hprod : ∀ (κp κm : PartialPairing (Fin m)), MeasureTheory.Integrable (fun (ω : M.Ω) => pmPairingCoeff M ρ lam ε m α β κp ω * (starRingEnd ℂ) (pmPairingCoeff M ρ lam ε m α β κm ω)) MeasureTheory.volume) : MeasureTheory.MemLp (pmCoeff M ρ lam ε m α β) 2 MeasureTheory.volume

The complete coefficient is in L² once the minimal spatial expansion condition and all pairwise expectation integrability conditions hold.

theorem Anderson4D.integral_norm_sq_pmCoeff_eq_sum_pairingProducts {M : NoiseModel} {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {α β : Z4} (hspatial : PairingCoefficientSpatialIntegrable M ρ lam ε m α β) (hprod : ∀ (κp κm : PartialPairing (Fin m)), MeasureTheory.Integrable (fun (ω : M.Ω) => pmPairingCoeff M ρ lam ε m α β κp ω * (starRingEnd ℂ) (pmPairingCoeff M ρ lam ε m α β κm ω)) MeasureTheory.volume) : ↑(∫ (ω : M.Ω), ‖pmCoeff M ρ lam ε m α β ω‖ ^ 2) = ∑ κp : PartialPairing (Fin m), ∑ κm : PartialPairing (Fin m), ∫ (ω : M.Ω), pmPairingCoeff M ρ lam ε m α β κp ω * (starRingEnd ℂ) (pmPairingCoeff M ρ lam ε m α β κm ω)

Pure finite-sum expectation algebra: after coefficient expansion, the squared norm expectation is the double sum of pairing-product expectations. No spatial Fubini exchange occurs in this theorem.

theorem Anderson4D.pmCoeffMomentFubiniOutput_of_spatial {M : NoiseModel} {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {α β : Z4} (hspatial : PairingCoefficientSpatialIntegrable M ρ lam ε m α β) (hprod : ∀ (κp κm : PartialPairing (Fin m)), MeasureTheory.Integrable (fun (ω : M.Ω) => pmPairingCoeff M ρ lam ε m α β κp ω * (starRingEnd ℂ) (pmPairingCoeff M ρ lam ε m α β κm ω)) MeasureTheory.volume) (hfubini : ∀ (κp κm : PartialPairing (Fin m)), ∫ (ω : M.Ω), pmPairingCoeff M ρ lam ε m α β κp ω * (starRingEnd ℂ) (pmPairingCoeff M ρ lam ε m α β κm ω) = expectedWickMomentPairingTerm M ρ lam ε m α β κp κm) (hjoint : ∀ (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles), MeasureTheory.Integrable (r324Flatten (deterministicMomentIntegrand ρ ε m α β κp κm π)) (r324PhysicalMeasure m)) : PmCoeffMomentFubiniOutput M ρ lam ε m α β

Constructor for the full Fubini output that discharges its coefficient expansion and measurability fields from explicit constructions. The remaining arguments are precisely the unresolved absolute-integrability, spatial Fubini, and deterministic joint-integrability obligations.