Measurability for individual parametrix pairing coefficients #
This file supplies the measurable half of the spatial Fubini interface used in the second-moment reduction.
theorem
Anderson4D.measurable_detIntegrand
(ρ : SmoothCutoff)
(ε : ℝ)
{m : ℕ}
(κ : PartialPairing (Fin m))
:
Measurable fun (xt : Fin (m + 2) → T4) => detIntegrand ρ ε m κ xt
The deterministic closed-form parametrix integrand is measurable in all of its assembled spatial coordinates.
theorem
Anderson4D.NoiseModel.measurable_wickAt_joint
(M : NoiseModel)
(ρ : SmoothCutoff)
(ε : ℝ)
{m : ℕ}
(κ : PartialPairing (Fin m))
:
wickAt is jointly measurable in the sample and its complete spatial
tuple.
theorem
Anderson4D.NoiseModel.measurable_randIntegrand_joint
(M : NoiseModel)
(ρ : SmoothCutoff)
(ε : ℝ)
{m : ℕ}
(κ : PartialPairing (Fin m))
:
Measurable fun (p : M.Ω × (Fin (m + 2) → T4)) => randIntegrand M ρ ε κ p.2 p.1
The random renormalized integrand is jointly measurable in the sample and its assembled spatial tuple.
theorem
Anderson4D.NoiseModel.measurable_randRI_joint
(M : NoiseModel)
(ρ : SmoothCutoff)
(lam ε : ℝ)
(m : ℕ)
(κ : PartialPairing (Fin m))
:
A single random pairing kernel is jointly measurable in the sample and its two external points.
theorem
Anderson4D.NoiseModel.measurable_pmPairingCoeff
(M : NoiseModel)
(ρ : SmoothCutoff)
(lam ε : ℝ)
(m : ℕ)
(α β : Z4)
(κ : PartialPairing (Fin m))
:
Measurable (pmPairingCoeff M ρ lam ε m α β κ)
Every individual pairing contribution to a Fourier coefficient is measurable in the noise sample.
theorem
Anderson4D.NoiseModel.aestronglyMeasurable_pmPairingCoeff
(M : NoiseModel)
(ρ : SmoothCutoff)
(lam ε : ℝ)
(m : ℕ)
(α β : Z4)
(κ : PartialPairing (Fin m))
:
MeasureTheory.AEStronglyMeasurable (pmPairingCoeff M ρ lam ε m α β κ) MeasureTheory.volume
The measurable field of PmCoeffMomentFubiniOutput is unconditional:
it follows directly from the explicit Fourier-series construction.