Uniform spatial bounds for the parametrix Wick factors

The pointwise Wick law is not by itself enough to exchange the noise and physical integrations in the second-moment calculation. This file records the missing uniform ingredient. At fixed mollification scale the covariance is bounded uniformly on the torus, hence the second moment of every fixed finite Wick factor is bounded uniformly in all of its spatial labels.

theorem Anderson4D.NoiseModel.integral_wickAt_mul_eq_crossSingles (M : NoiseModel) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) {m : ℕ} (κp κm : PartialPairing (Fin m)) (xtp xtm : Fin (m + 2) → T4) : ∫ (ω : M.Ω), wickAt M ρ ε κp xtp ω * wickAt M ρ ε κm xtm ω = crossSinglesEquivCovarianceSum κp κm fun (i : ↥κp.singles) (j : ↥κm.singles) => ρ.etaEpsT4 ε (xtp (varIdx ↑i) - xtm (varIdx ↑j))

Exact cross-contraction formula for two wickAt factors with arbitrary spatial tuples.

theorem Anderson4D.NoiseModel.integrable_wickAt_mul (M : NoiseModel) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) {m : ℕ} (κp κm : PartialPairing (Fin m)) (xtp xtm : Fin (m + 2) → T4) : MeasureTheory.Integrable (fun (ω : M.Ω) => wickAt M ρ ε κp xtp ω * wickAt M ρ ε κm xtm ω) MeasureTheory.volume

Products of two wickAt factors are integrable for every fixed pair of spatial tuples.

theorem Anderson4D.NoiseModel.crossSingles_self_le_of_covariance_bound (ρ : SmoothCutoff) (ε B : ℝ) {m : ℕ} (κ : PartialPairing (Fin m)) (hB : ∀ (z : T4), ρ.etaEpsT4 ε z ≤ B) (xt : Fin (m + 2) → T4) : (crossSinglesEquivCovarianceSum κ κ fun (i j : ↥κ.singles) => ρ.etaEpsT4 ε (xt (varIdx ↑i) - xt (varIdx ↑j))) ≤ ∑ _π : ↥κ.singles ≃ ↥κ.singles, ∏ _i : ↥κ.singles, B

A uniform covariance bound controls the diagonal cross-contraction sum of one Wick factor, independently of its spatial labels.

theorem Anderson4D.NoiseModel.exists_uniform_integral_sq_wickAt_bound (M : NoiseModel) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} (κ : PartialPairing (Fin m)) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (xt : Fin (m + 2) → T4), ∫ (ω : M.Ω), wickAt M ρ ε κ xt ω ^ 2 ≤ C

The second moment of a fixed Wick factor admits a finite uniform bound over every choice of its spatial labels.

theorem Anderson4D.NoiseModel.exists_uniform_integral_norm_wickAt_mul_bound (M : NoiseModel) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} (κp κm : PartialPairing (Fin m)) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (xtp xtm : Fin (m + 2) → T4), ∫ (ω : M.Ω), ‖wickAt M ρ ε κp xtp ω * wickAt M ρ ε κm xtm ω‖ ≤ C

The absolute first moment of a product of two Wick factors is uniformly bounded in both spatial tuples. This is the domination used in the noise-by-space Tonelli argument.

theorem Anderson4D.NoiseModel.exists_uniform_norm_wickAt_bound_of_continuous (M : NoiseModel) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} (κ : PartialPairing (Fin m)) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) : ∃ (B : ℝ), 0 ≤ B ∧ ∀ (xt : Fin (m + 2) → T4), |wickAt M ρ ε κ xt ω| ≤ B

On every continuous noise sample, wickAt is bounded uniformly over all of its spatial labels.