Global integrability of random pairing profiles

At positive mollification scale, every deterministic pairing profile is jointly integrable in both endpoints and all internal variables. On a continuous noise sample its Wick factor is uniformly bounded, so the full random pairing profile is jointly integrable as well. This is the global analytic input needed to turn the pointwise ledgers in Proposition 3.4 into almost-everywhere endpoint statements.

theorem Anderson4D.NoiseModel.integrable_randIntegrand_flat (M : NoiseModel) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (m : ℕ) (κ : PartialPairing (Fin m)) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) : MeasureTheory.Integrable (fun (p : PairingHalfPhysicalPoint m) => ↑(randIntegrand M ρ ε κ (assemble p.1 p.2.1 p.2.2) ω)) (pairingHalfPhysicalMeasure m)

On every continuous mollified-noise sample, one complete random pairing profile is jointly integrable in both external endpoints and all internal variables.

theorem Anderson4D.NoiseModel.ae_ae_integrable_randIntegrand (M : NoiseModel) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (m : ℕ) (κ : PartialPairing (Fin m)) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) : ∀ᵐ (x : T4) (y : T4) ∂paperMeasure, MeasureTheory.Integrable (fun (v : Fin m → T4) => ↑(randIntegrand M ρ ε κ (assemble x y v) ω)) (MeasureTheory.Measure.pi fun (x : Fin m) => paperMeasure)

Global integrability supplies the correct almost-everywhere fixed-endpoint internal-integrability statement. No assertion is made on the exceptional endpoint diagonal.

theorem Anderson4D.NoiseModel.ae_ae_integrable_randIntegrand_all (M : NoiseModel) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (m : ℕ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) : ∀ᵐ (x : T4) (y : T4) ∂paperMeasure, ∀ (κ : PartialPairing (Fin m)), MeasureTheory.Integrable (fun (v : Fin m → T4) => ↑(randIntegrand M ρ ε κ (assemble x y v) ω)) (MeasureTheory.Measure.pi fun (x : Fin m) => paperMeasure)

The preceding endpoint statement holds simultaneously for the finite family of all partial pairings at a fixed order.