Noise--space Fubini for one doubled parametrix pairing

This file realizes the analytic Fubini output used in paper (3.24). The six physical variable groups are represented as four external points and one doubled internal tuple. The two copies are joined by the measure-preserving Fin m + Fin m = Fin (2m) reindexing.

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

Complex spatial integrand of one within-copy pairing, without its coupling factor.

Equations

• Anderson4D.pairingHalfIntegrand M ρ ε m α β κ ω x y v = Anderson4D.charT4 α x * Anderson4D.charT4 β y * ↑(Anderson4D.randIntegrand M ρ ε κ (Anderson4D.assemble x y v) ω)

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

Frozen iterated physical integral of one pairing before multiplication by λ_ε^m.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.pmPairingCoeff_eq_lam_pow_mul_pairingHalfIntegral (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (α β : Z4) (κ : PartialPairing (Fin m)) (ω : M.Ω) : pmPairingCoeff M ρ lam ε m α β κ ω = ↑(lamEps lam ε) ^ m * pairingHalfIntegral M ρ ε m α β κ ω

One pairing coefficient is its unscaled physical integral times the common coupling power.

theorem Anderson4D.conj_pmPairingCoeff (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (α β : Z4) (κ : PartialPairing (Fin m)) (ω : M.Ω) : (starRingEnd ℂ) (pmPairingCoeff M ρ lam ε m α β κ ω) = pmPairingCoeff M ρ lam ε m (-α) (-β) κ ω

Negating both Fourier modes conjugates an individual pairing coefficient.

The doubled finite tuple

def Anderson4D.momentDoublePiMeasurableEquiv (m : ℕ) (X : Type u_1) [MeasurableSpace X] : (Fin (2 * m) → X) ≃ᵐ (Fin m → X) × (Fin m → X)

Split the doubled internal tuple into its left and right copies.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Anderson4D.momentDoublePiMeasurableEquiv_apply (m : ℕ) (X : Type u_1) [MeasurableSpace X] (v : Fin (2 * m) → X) : (momentDoublePiMeasurableEquiv m X) v = (fun (i : Fin m) => v (leftMomentIndex i), fun (j : Fin m) => v (rightMomentIndex j))

theorem Anderson4D.measurePreserving_momentDoublePi (m : ℕ) : MeasureTheory.MeasurePreserving (⇑(momentDoublePiMeasurableEquiv m T4)) (MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure) ((MeasureTheory.Measure.pi fun (x : Fin m) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : Fin m) => paperMeasure))

The doubled-tuple split preserves the corresponding product Haar measure.

theorem Anderson4D.integral_momentDouble_mul (m : ℕ) (f g : (Fin m → T4) → ℂ) : (∫ (v : Fin (2 * m) → T4), (f fun (i : Fin m) => v (leftMomentIndex i)) * g fun (j : Fin m) => v (rightMomentIndex j) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure) = (∫ (u : Fin m → T4), f u ∂MeasureTheory.Measure.pi fun (x : Fin m) => paperMeasure) * ∫ (t : Fin m → T4), g t ∂MeasureTheory.Measure.pi fun (x : Fin m) => paperMeasure

A complex separated integrand factors after the concrete doubled-tuple split.

noncomputable def Anderson4D.pairingMomentRaw (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (ω : M.Ω) (x y z w : T4) (v : Fin (2 * m) → T4) : ℂ

The unscaled doubled physical integrand at one noise sample.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Anderson4D.pairingMomentRawSpatialIntegral (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (ω : M.Ω) : ℂ

Frozen five-fold physical integral of the doubled raw integrand.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.pairingMomentRawSpatialIntegral_eq_mul (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (ω : M.Ω) : pairingMomentRawSpatialIntegral M ρ ε m α β κp κm ω = pairingHalfIntegral M ρ ε m α β κp ω * pairingHalfIntegral M ρ ε m (-α) (-β) κm ω

The doubled physical integral factors into the two copy integrals. This identity is valid for totalized integrals and needs no sectionwise integrability premise.

theorem Anderson4D.pmPairingCoeff_mul_conj_eq_rawSpatialIntegral (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (ω : M.Ω) : pmPairingCoeff M ρ lam ε m α β κp ω * (starRingEnd ℂ) (pmPairingCoeff M ρ lam ε m α β κm ω) = ↑(lamEps lam ε) ^ (2 * m) * pairingMomentRawSpatialIntegral M ρ ε m α β κp κm ω

Product of two individual pairing coefficients as a scalar multiple of the doubled raw physical integral.

Joint noise--space integrand

@[reducible, inline]

abbrev Anderson4D.PairingHalfPoint (M : NoiseModel) (m : ℕ) : Type

Left-associated carrier for one unintegrated pairing half.

Equations

• Anderson4D.PairingHalfPoint M m = (((M.Ω × Anderson4D.T4) × Anderson4D.T4) × (Fin m → Anderson4D.T4))

def Anderson4D.pairingHalfTupleMap (M : NoiseModel) (m : ℕ) : PairingHalfPoint M m → M.Ω × (Fin (m + 2) → T4)

Assemble the noise sample and all spatial variables of one pairing half into the carrier used by the joint random-integrand theorem.

Equations

• Anderson4D.pairingHalfTupleMap M m p = (p.1.1.1, Anderson4D.assemble p.1.1.2 p.1.2 p.2)

theorem Anderson4D.measurable_pairingHalfTupleMap (M : NoiseModel) (m : ℕ) : Measurable (pairingHalfTupleMap M m)

def Anderson4D.pairingMomentLeftPoint (M : NoiseModel) (m : ℕ) : M.Ω × R324PhysicalPoint m → PairingHalfPoint M m

Select the left copy of the doubled physical tuple.

Equations

• Anderson4D.pairingMomentLeftPoint M m p = (((p.1, p.2.1), p.2.2.1), fun (i : Fin m) => p.2.2.2.2.2 (Anderson4D.leftMomentIndex i))

theorem Anderson4D.measurable_pairingMomentLeftPoint (M : NoiseModel) (m : ℕ) : Measurable (pairingMomentLeftPoint M m)

def Anderson4D.pairingMomentRightPoint (M : NoiseModel) (m : ℕ) : M.Ω × R324PhysicalPoint m → PairingHalfPoint M m

Select the right copy of the doubled physical tuple.

Equations

• Anderson4D.pairingMomentRightPoint M m p = (((p.1, p.2.2.2.1), p.2.2.2.2.1), fun (i : Fin m) => p.2.2.2.2.2 (Anderson4D.rightMomentIndex i))

theorem Anderson4D.measurable_pairingMomentRightPoint (M : NoiseModel) (m : ℕ) : Measurable (pairingMomentRightPoint M m)

theorem Anderson4D.measurable_pairingHalfPhase (M : NoiseModel) (m : ℕ) (α β : Z4) : Measurable fun (p : PairingHalfPoint M m) => charT4 α p.1.1.2 * charT4 β p.1.2

The Fourier phase of one pairing half is measurable on its carrier.

noncomputable def Anderson4D.pairingHalfRandom (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (κ : PartialPairing (Fin m)) (p : PairingHalfPoint M m) : ℂ

Named random factor of one pairing half. Naming the composition avoids forcing the elaborator to unfold the full Wick polynomial during every measurability composition.

Equations

• Anderson4D.pairingHalfRandom M ρ ε m κ p = ↑(Anderson4D.randIntegrand M ρ ε κ (Anderson4D.pairingHalfTupleMap M m p).2 (Anderson4D.pairingHalfTupleMap M m p).1)

theorem Anderson4D.NoiseModel.measurable_pairingHalfRandom (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (κ : PartialPairing (Fin m)) : Measurable (pairingHalfRandom M ρ ε m κ)

theorem Anderson4D.NoiseModel.measurable_pairingHalfIntegrand_joint (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (κ : PartialPairing (Fin m)) : Measurable fun (p : PairingHalfPoint M m) => pairingHalfIntegrand M ρ ε m α β κ p.1.1.1 p.1.1.2 p.1.2 p.2

Joint measurability of one unscaled pairing half.

noncomputable def Anderson4D.pairingMomentRawFlatten (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (p : M.Ω × R324PhysicalPoint m) : ℂ

Flatten the random doubled integrand onto noise times the genuine R-324 physical product space.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Anderson4D.pairingMomentRawFlatten_apply (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (ω : M.Ω) (p : R324PhysicalPoint m) : pairingMomentRawFlatten M ρ ε m α β κp κm (ω, p) = r324Flatten (pairingMomentRaw M ρ ε m α β κp κm ω) p

theorem Anderson4D.NoiseModel.measurable_pairingMomentRawFlatten (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (κp κm : PartialPairing (Fin m)) : Measurable (pairingMomentRawFlatten M ρ ε m α β κp κm)

The raw doubled moment integrand is jointly Borel measurable in the noise sample and all physical variables.

theorem Anderson4D.integral_pairingMomentRaw_eq_expectedWickMomentIntegrand (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (x y z w : T4) (v : Fin (2 * m) → T4) : ∫ (ω : M.Ω), pairingMomentRaw M ρ ε m α β κp κm ω x y z w v = expectedWickMomentIntegrand M ρ ε m α β κp κm x y z w v

Integrating the raw doubled integrand in the noise variable gives the named expected Wick moment integrand.

def Anderson4D.PairingMomentRawIntegrable (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (κp κm : PartialPairing (Fin m)) : Prop

Joint noise--space integrability is the single analytic premise needed to obtain both integrability of a pairing-coefficient product and its exact Fubini expansion.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.pairingProduct_integrable_of_raw (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (hraw : PairingMomentRawIntegrable M ρ ε m α β κp κm) : MeasureTheory.Integrable (fun (ω : M.Ω) => pmPairingCoeff M ρ lam ε m α β κp ω * (starRingEnd ℂ) (pmPairingCoeff M ρ lam ε m α β κm ω)) MeasureTheory.volume

Joint integrability of the raw noise--space term implies integrability of the corresponding product of Fourier coefficients.

theorem Anderson4D.pairingProduct_fubini_of_raw (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (hraw : PairingMomentRawIntegrable M ρ ε m α β κp κm) : ∫ (ω : M.Ω), pmPairingCoeff M ρ lam ε m α β κp ω * (starRingEnd ℂ) (pmPairingCoeff M ρ lam ε m α β κm ω) = expectedWickMomentPairingTerm M ρ lam ε m α β κp κm

Joint integrability gives the exact noise--space Fubini identity for one pair (κp,κm).

Discharging joint integrability by uniform Wick domination

noncomputable def Anderson4D.pairingMomentDeterministicFactor (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (x y z w : T4) (v : Fin (2 * m) → T4) : ℂ

Deterministic factor of the raw pairing moment, before the two Wick factors are attached.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.pairingMomentRaw_eq_deterministic_mul_wick (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (ω : M.Ω) (x y z w : T4) (v : Fin (2 * m) → T4) : pairingMomentRaw M ρ ε m α β κp κm ω x y z w v = pairingMomentDeterministicFactor ρ ε m α β κp κm x y z w v * ↑(pairedWickProduct M ρ ε m κp κm x y z w v ω)

The raw random term is the deterministic factor times the paired Wick product.

theorem Anderson4D.pairingMomentRawIntegrable_of_deterministic (M : NoiseModel) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (m : ℕ) (α β : Z4) (κp κm : PartialPairing (Fin m)) (hdet : MeasureTheory.Integrable (r324Flatten (pairingMomentDeterministicFactor ρ ε m α β κp κm)) (r324PhysicalMeasure m)) : PairingMomentRawIntegrable M ρ ε m α β κp κm

Joint integrability of the deterministic doubled profile, together with the uniform Wick second-moment bound, implies full noise--space integrability.