Closing the analytic interfaces in the parametrix second moment

The low-level noise--space Fubini theorem reduces the random calculation to deterministic joint integrability. This file packages that reduction into the exact PmCoeffMomentFubiniOutput consumed by P-3.5b.

noncomputable def Anderson4D.pairingHalfPhysicalMeasure (m : ℕ) : MeasureTheory.Measure (T4 × T4 × (Fin m → T4))

Flat product measure for one copy of an order-m parametrix profile.

Equations

• Anderson4D.pairingHalfPhysicalMeasure m = Anderson4D.paperMeasure.prod (Anderson4D.paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin m) => Anderson4D.paperMeasure))

instance Anderson4D.instSFinitePairingHalfPhysicalMeasure (m : ℕ) : MeasureTheory.SFinite (pairingHalfPhysicalMeasure m)

@[reducible, inline]

abbrev Anderson4D.PairingHalfPhysicalPoint (m : ℕ) : Type

Spatial carrier for one flat deterministic profile.

Equations

• Anderson4D.PairingHalfPhysicalPoint m = (Anderson4D.T4 × Anderson4D.T4 × (Fin m → Anderson4D.T4))

def Anderson4D.pairingHalfFixedTupleMap (M : NoiseModel) (m : ℕ) (ω : M.Ω) : PairingHalfPhysicalPoint m → M.Ω × (Fin (m + 2) → T4)

Insert a fixed noise sample into one flat physical profile.

Equations

• Anderson4D.pairingHalfFixedTupleMap M m ω p = (ω, Anderson4D.assemble p.1 p.2.1 p.2.2)

theorem Anderson4D.measurable_pairingHalfFixedTupleMap (M : NoiseModel) (m : ℕ) (ω : M.Ω) : Measurable (pairingHalfFixedTupleMap M m ω)

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

Unit-modulus Fourier phase times the Wick factor at a fixed sample.

Equations

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

theorem Anderson4D.NoiseModel.measurable_pairingHalfWickWeight (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) (κ : PartialPairing (Fin m)) (ω : M.Ω) : Measurable (pairingHalfWickWeight M ρ ε m α β κ ω)

theorem Anderson4D.pairingCoefficientSpatialIntegrable_of_detIntegrand_flat (M : NoiseModel) (ρ : SmoothCutoff) (lam : ℝ) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (m : ℕ) (α β : Z4) (hdet : ∀ (κ : PartialPairing (Fin m)), MeasureTheory.Integrable (fun (p : T4 × T4 × (Fin m → T4)) => ↑(detIntegrand ρ ε m κ (assemble p.1 p.2.1 p.2.2))) (pairingHalfPhysicalMeasure m)) : PairingCoefficientSpatialIntegrable M ρ lam ε m α β

A deterministic flat-profile integrability theorem yields the minimal spatial hypothesis needed for the finite pairing expansion, on the almost-sure event where the mollified noise is continuous.

theorem Anderson4D.pmCoeffMomentFubiniOutput_of_deterministic_integrability (M : NoiseModel) (ρ : SmoothCutoff) (lam : ℝ) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (m : ℕ) (α β : Z4) (hhalf : ∀ (κ : PartialPairing (Fin m)), MeasureTheory.Integrable (fun (p : T4 × T4 × (Fin m → T4)) => ↑(detIntegrand ρ ε m κ (assemble p.1 p.2.1 p.2.2))) (pairingHalfPhysicalMeasure m)) (hbare : ∀ (κp κm : PartialPairing (Fin m)), MeasureTheory.Integrable (r324Flatten (pairingMomentDeterministicFactor ρ ε m α β κp κm)) (r324PhysicalMeasure m)) (hcross : ∀ (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles), MeasureTheory.Integrable (r324Flatten (deterministicMomentIntegrand ρ ε m α β κp κm π)) (r324PhysicalMeasure m)) : PmCoeffMomentFubiniOutput M ρ lam ε m α β

Complete P-3.5b Fubini output from deterministic flat and doubled integrability. No random-level estimate is assumed.