Wick orthogonality for the mollified noise

This file instantiates the generic polynomial Wick theorem for xiEps, then specializes it to the two wickAt factors in the random parametrix.

theorem Anderson4D.NoiseModel.hasGaussianLaw_xiEps (M : NoiseModel) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (z : T4) : ProbabilityTheory.HasGaussianLaw (fun (ω : M.Ω) => M.xiEps ρ ε ω z) MeasureTheory.volume

theorem Anderson4D.NoiseModel.memLp_xiEps (M : NoiseModel) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (z : T4) (p : ENNReal) (hp : p ≠ ⊤) : MeasureTheory.MemLp (fun (ω : M.Ω) => M.xiEps ρ ε ω z) p MeasureTheory.volume

theorem Anderson4D.NoiseModel.integrable_xiEpsProduct (M : NoiseModel) {r : ℕ} (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (z : Fin r → T4) : MeasureTheory.Integrable (fun (ω : M.Ω) => ∏ i : Fin r, M.xiEps ρ ε ω (z i)) MeasureTheory.volume

theorem Anderson4D.NoiseModel.integrable_xiEpsListProduct (M : NoiseModel) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (zs : List T4) : MeasureTheory.Integrable (gaussianListProduct (fun (z : T4) (ω : M.Ω) => M.xiEps ρ ε ω z) zs) MeasureTheory.volume

theorem Anderson4D.NoiseModel.integral_xiEpsProduct_even_eq_wickPairingSum (M : NoiseModel) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (q : ℕ) (z : Fin (2 * q) → T4) : ∫ (ω : M.Ω), ∏ i : Fin (2 * q), M.xiEps ρ ε ω (z i) = wickPairingSum fun (i j : Fin (2 * q)) => ρ.etaEpsT4 ε (z i - z j)

theorem Anderson4D.NoiseModel.integral_xiEpsProduct_odd_eq_zero (M : NoiseModel) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (q : ℕ) (z : Fin (2 * q + 1) → T4) : ∫ (ω : M.Ω), ∏ i : Fin (2 * q + 1), M.xiEps ρ ε ω (z i) = 0

theorem Anderson4D.NoiseModel.integral_xiEpsProduct_eq_wickPairingSum (M : NoiseModel) {r : ℕ} (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (z : Fin r → T4) : ∫ (ω : M.Ω), ∏ i : Fin r, M.xiEps ρ ε ω (z i) = wickPairingSum fun (i j : Fin r) => ρ.etaEpsT4 ε (z i - z j)

theorem Anderson4D.NoiseModel.integral_xiEpsListProduct_eq_wickPairingList (M : NoiseModel) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (zs : List T4) : ∫ (ω : M.Ω), gaussianListProduct (fun (z : T4) (ω : M.Ω) => M.xiEps ρ ε ω z) zs ω = wickPairingList (fun (x y : T4) => ρ.etaEpsT4 ε (x - y)) zs

theorem Anderson4D.NoiseModel.gaussianListMomentLaw_xiEps (M : NoiseModel) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) : GaussianListMomentLaw MeasureTheory.volume (fun (x y : T4) => ρ.etaEpsT4 ε (x - y)) fun (x : T4) (ω : M.Ω) => M.xiEps ρ ε ω x

The whole spatial mollified-noise family satisfies the raw Isserlis list-moment interface.

theorem Anderson4D.NoiseModel.gaussianPolynomialLaw_xiEps (M : NoiseModel) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) : GaussianPolynomialLaw MeasureTheory.volume (fun (x y : T4) => ρ.etaEpsT4 ε (x - y)) fun (x : T4) (ω : M.Ω) => M.xiEps ρ ε ω x

Polynomial Gaussian integration by parts for the mollified noise.

theorem Anderson4D.NoiseModel.integral_wickPolynomial_xiEps_mul (M : NoiseModel) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (xs ys : List T4) : ∫ (ω : M.Ω), wickPolynomial (fun (x y : T4) => ρ.etaEpsT4 ε (x - y)) (fun (x : T4) (ω' : M.Ω) => M.xiEps ρ ε ω' x) xs ω * wickPolynomial (fun (x y : T4) => ρ.etaEpsT4 ε (x - y)) (fun (x : T4) (ω' : M.Ω) => M.xiEps ρ ε ω' x) ys ω = crossWickList (fun (x y : T4) => ρ.etaEpsT4 ε (x - y)) xs ys

Exact cross-contraction formula for two Wick polynomials of the mollified noise.

theorem Anderson4D.NoiseModel.integrable_wickPolynomial_xiEps_mul (M : NoiseModel) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (xs ys : List T4) : MeasureTheory.Integrable (fun (ω : M.Ω) => wickPolynomial (fun (x y : T4) => ρ.etaEpsT4 ε (x - y)) (fun (x : T4) (ω' : M.Ω) => M.xiEps ρ ε ω' x) xs ω * wickPolynomial (fun (x y : T4) => ρ.etaEpsT4 ε (x - y)) (fun (x : T4) (ω' : M.Ω) => M.xiEps ρ ε ω' x) ys ω) MeasureTheory.volume

Products of two mollified-noise Wick polynomials are integrable.