Probabilistic second-moment reduction for the parametrix coefficients

This file isolates the probabilistic content of Deng--Shen (3.24) from the deterministic R-324 estimate.

There are two genuinely upstream analytic inputs:

• WickAtSecondMomentLaw is the specialization of P-wick to the two Wick products occurring in the two copies of the order-m kernel. Its right side uses the exact κp.singles ≃ κm.singles representation consumed by deterministicMomentPairingSum.
• PmCoeffMomentFubiniOutput records only the Fubini/integrability output needed to flatten the square of the iterated, junk-totalized coefficient. In particular it does not contain a deterministic bound or the desired second-moment equality.

From those inputs we prove the exact identity

E ‖pmCoeff m α β‖² = deterministicMomentPairingSum ρ λ ε m α β,

with the real expectation coerced to ℂ. The final theorems then consume the existing P-3.5b-det interface and expose both MemLp 2 and the squared geometric form expected by Main/GeometricTruncation.lean.

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

The contribution of one within-copy partial pairing to the Fourier coefficient. This is deliberately expressed with the already frozen randRI, so the only operation hidden here is the two external integrals.

Equations

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

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

The two Wick factors evaluated on the left and right copies of the doubled internal carrier.

Equations

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

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

The random part of one doubled contraction after expectation, but before the cross-single Wick contractions are expanded.

Equations

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

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

The flattened expected contribution of one pair (κp, κm), including the common coupling λ_ε^(2m).

Equations

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

structure Anderson4D.NestedMomentIntegrable {m : ℕ} (f : T4 → T4 → T4 → T4 → (Fin (2 * m) → T4) → ℂ) : Prop

A stronger nested-integrability condition. It is useful for local algebra but is not required by the public second-moment interface: exceptional Green diagonals prevent constructing these fields uniformly at every fixed outer point.

• internal (x y z w : T4) : MeasureTheory.Integrable (f x y z w) (MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure)
• w (x y z : T4) : MeasureTheory.Integrable (fun (w : T4) => ∫ (v : Fin (2 * m) → T4), f x y z w v ∂MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure) paperMeasure
• z (x y : T4) : MeasureTheory.Integrable (fun (z : T4) => ∫ (w : T4), ∫ (v : Fin (2 * m) → T4), f x y z w v ∂MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure ∂paperMeasure) paperMeasure
• y (x : T4) : MeasureTheory.Integrable (fun (y : T4) => ∫ (z : T4), ∫ (w : T4), ∫ (v : Fin (2 * m) → T4), f x y z w v ∂MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure ∂paperMeasure ∂paperMeasure) paperMeasure
• x : MeasureTheory.Integrable (fun (x : T4) => ∫ (y : T4), ∫ (z : T4), ∫ (w : T4), ∫ (v : Fin (2 * m) → T4), f x y z w v ∂MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure ∂paperMeasure ∂paperMeasure ∂paperMeasure) paperMeasure

theorem Anderson4D.integral_five_finsetSum {ι : Type u_1} {m : ℕ} (s : Finset ι) (f : ι → T4 → T4 → T4 → T4 → (Fin (2 * m) → T4) → ℂ) (hf : ∀ i ∈ s, NestedMomentIntegrable (f i)) : ∫ (x : T4), ∫ (y : T4), ∫ (z : T4), ∫ (w : T4), ∫ (v : Fin (2 * m) → T4), ∑ i ∈ s, f i x y z w v ∂MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure ∂paperMeasure ∂paperMeasure ∂paperMeasure ∂paperMeasure = ∑ i ∈ s, ∫ (x : T4), ∫ (y : T4), ∫ (z : T4), ∫ (w : T4), ∫ (v : Fin (2 * m) → T4), f i x y z w v ∂MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure ∂paperMeasure ∂paperMeasure ∂paperMeasure ∂paperMeasure

A finite sum may be moved through the frozen five-fold spatial integral under the all-sections condition.

theorem Anderson4D.integral_five_finsetSum_joint {ι : Type u_1} {m : ℕ} (s : Finset ι) (f : ι → T4 → T4 → T4 → T4 → (Fin (2 * m) → T4) → ℂ) (hf : ∀ i ∈ s, MeasureTheory.Integrable (r324Flatten (f i)) (r324PhysicalMeasure m)) : ∫ (x : T4), ∫ (y : T4), ∫ (z : T4), ∫ (w : T4), ∫ (v : Fin (2 * m) → T4), ∑ i ∈ s, f i x y z w v ∂MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure ∂paperMeasure ∂paperMeasure ∂paperMeasure ∂paperMeasure = ∑ i ∈ s, ∫ (x : T4), ∫ (y : T4), ∫ (z : T4), ∫ (w : T4), ∫ (v : Fin (2 * m) → T4), f i x y z w v ∂MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure ∂paperMeasure ∂paperMeasure ∂paperMeasure ∂paperMeasure

Correct joint-product-space version of the preceding finite-sum Fubini lemma. It makes no assertion about exceptional fixed sections.

structure Anderson4D.WickAtSecondMomentLaw (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) : Prop

The missing P-wick specialization.

This is strictly a noise-law statement: it has no Green kernels, spatial integrals, Fourier characters, coupling constants, or target bounds. The expectation of the two Wick polynomials is the sum over bijections between their single sets. Unequal chaos orders give the empty Equiv sum.

• integrable (κp κm : PartialPairing (Fin m)) (x y z w : T4) (v : Fin (2 * m) → T4) : MeasureTheory.Integrable (pairedWickProduct M ρ ε m κp κm x y z w v) MeasureTheory.volume
• expectation (κp κm : PartialPairing (Fin m)) (x y z w : T4) (v : Fin (2 * m) → T4) : ∫ (ω : M.Ω), pairedWickProduct M ρ ε m κp κm x y z w v ω = crossSinglesEquivCovarianceSum κp κm fun (i : ↥κp.singles) (j : ↥κm.singles) => ρ.etaEpsT4 ε (v (leftMomentIndex ↑i) - v (rightMomentIndex ↑j))

theorem Anderson4D.crossSinglesEquivCovarianceSum_eq_momentCrossCovarianceSum (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (κp κm : PartialPairing (Fin m)) (v : Fin (2 * m) → T4) : (crossSinglesEquivCovarianceSum κp κm fun (i : ↥κp.singles) (j : ↥κm.singles) => ρ.etaEpsT4 ε (v (leftMomentIndex ↑i) - v (rightMomentIndex ↑j))) = ∑ π : ↥κp.singles ≃ ↥κm.singles, momentCrossCovarianceProduct ρ ε m κp κm π v

The right side of WickAtSecondMomentLaw.expectation is definitionally the finite cross-contraction sum used by the deterministic moment kernel.

structure Anderson4D.PmCoeffMomentFubiniOutput (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (α β : Z4) : Prop

Purely analytic output needed to flatten the square of pmCoeff.

The last field licenses the finite cross-contraction sum exchanges after P-wick is applied. No field mentions deterministicMomentPairingSum, its norm, deterministicMomentRHS, or a second-moment bound.

• coefficient_expansion : pmCoeff M ρ lam ε m α β =ᵐ[MeasureTheory.volume] fun (ω : M.Ω) => ∑ κ : PartialPairing (Fin m), pmPairingCoeff M ρ lam ε m α β κ ω
• pairingCoeff_aestronglyMeasurable (κ : PartialPairing (Fin m)) : MeasureTheory.AEStronglyMeasurable (pmPairingCoeff M ρ lam ε m α β κ) MeasureTheory.volume
• pairingProduct_integrable (κp κm : PartialPairing (Fin m)) : MeasureTheory.Integrable (fun (ω : M.Ω) => pmPairingCoeff M ρ lam ε m α β κp ω * (starRingEnd ℂ) (pmPairingCoeff M ρ lam ε m α β κm ω)) MeasureTheory.volume
• pairingProduct_fubini (κp κm : PartialPairing (Fin m)) : ∫ (ω : M.Ω), pmPairingCoeff M ρ lam ε m α β κp ω * (starRingEnd ℂ) (pmPairingCoeff M ρ lam ε m α β κm ω) = expectedWickMomentPairingTerm M ρ lam ε m α β κp κm
• deterministic_joint_integrable (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : MeasureTheory.Integrable (r324Flatten (deterministicMomentIntegrand ρ ε m α β κp κm π)) (r324PhysicalMeasure m)

theorem Anderson4D.expectedWickMomentPairingTerm_eq_sum {M : NoiseModel} {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {α β : Z4} (hwick : WickAtSecondMomentLaw M ρ ε m) (hjoint : ∀ (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles), MeasureTheory.Integrable (r324Flatten (deterministicMomentIntegrand ρ ε m α β κp κm π)) (r324PhysicalMeasure m)) (κp κm : PartialPairing (Fin m)) : expectedWickMomentPairingTerm M ρ lam ε m α β κp κm = ↑(lamEps lam ε) ^ (2 * m) * ∑ π : ↥κp.singles ≃ ↥κm.singles, deterministicMomentPairingTerm ρ ε m α β κp κm π

P-wick turns one flattened random pairing term into the sum of all its deterministic cross-single contractions.

theorem Anderson4D.PmCoeffMomentFubiniOutput.memLp_pairingCoeff {M : NoiseModel} {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {α β : Z4} (h : PmCoeffMomentFubiniOutput M ρ lam ε m α β) (κ : PartialPairing (Fin m)) : MeasureTheory.MemLp (pmPairingCoeff M ρ lam ε m α β κ) 2 MeasureTheory.volume

Every single pairing coefficient is in L² once all pairwise products in the Fubini output are integrable.

theorem Anderson4D.PmCoeffMomentFubiniOutput.memLp_pmCoeff {M : NoiseModel} {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {α β : Z4} (h : PmCoeffMomentFubiniOutput M ρ lam ε m α β) : MeasureTheory.MemLp (pmCoeff M ρ lam ε m α β) 2 MeasureTheory.volume

The complete coefficient is in L²; no MemLp premise is required by the final P-3.5b theorem.

theorem Anderson4D.integral_norm_sq_pmCoeff_eq_deterministicMomentPairingSum {M : NoiseModel} {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {α β : Z4} (hfubini : PmCoeffMomentFubiniOutput M ρ lam ε m α β) (hwick : WickAtSecondMomentLaw M ρ ε m) : ↑(∫ (ω : M.Ω), ‖pmCoeff M ρ lam ε m α β ω‖ ^ 2) = deterministicMomentPairingSum ρ lam ε m α β

Exact complex-valued second-moment identity. The left side is real but is coerced to ℂ so that it can be identified without discarding the Fourier phases in the deterministic pairing sum.

theorem Anderson4D.integral_norm_sq_pmCoeff_eq_re_deterministicMomentPairingSum {M : NoiseModel} {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {α β : Z4} (hfubini : PmCoeffMomentFubiniOutput M ρ lam ε m α β) (hwick : WickAtSecondMomentLaw M ρ ε m) : ∫ (ω : M.Ω), ‖pmCoeff M ρ lam ε m α β ω‖ ^ 2 = (deterministicMomentPairingSum ρ lam ε m α β).re

Real presentation of the exact second moment.

theorem Anderson4D.parametrix_coeff_memLp_and_second_moment_bound {M : NoiseModel} {ρ : SmoothCutoff} {outerConstant powerConstant lam ε : ℝ} {m : ℕ} {α β : Z4} (hfubini : PmCoeffMomentFubiniOutput M ρ lam ε m α β) (hwick : WickAtSecondMomentLaw M ρ ε m) (hdet : ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ deterministicMomentRHS outerConstant powerConstant lam ε m α β) : MeasureTheory.MemLp (pmCoeff M ρ lam ε m α β) 2 MeasureTheory.volume ∧ ∫ (ω : M.Ω), ‖pmCoeff M ρ lam ε m α β ω‖ ^ 2 ≤ deterministicMomentRHS outerConstant powerConstant lam ε m α β

P-3.5b / paper (3.24).

Once the exact P-wick and Fubini outputs are available, the only numerical premise is precisely the existing P-3.5b-det estimate on the frozen deterministic pairing sum. The conclusion simultaneously provides the MemLp 2 fact required downstream and the exact second absolute moment bound.

theorem Anderson4D.parametrix_coeff_bound {M : NoiseModel} {ρ : SmoothCutoff} {outerConstant powerConstant lam ε : ℝ} {m : ℕ} {α β : Z4} (hfubini : PmCoeffMomentFubiniOutput M ρ lam ε m α β) (hwick : WickAtSecondMomentLaw M ρ ε m) (hdet : ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ deterministicMomentRHS outerConstant powerConstant lam ε m α β) : MeasureTheory.MemLp (pmCoeff M ρ lam ε m α β) 2 MeasureTheory.volume ∧ ∫ (ω : M.Ω), ‖pmCoeff M ρ lam ε m α β ω‖ ^ 2 ≤ deterministicMomentRHS outerConstant powerConstant lam ε m α β

Blueprint endpoint P-3.5b.

theorem Anderson4D.exists_parametrix_coeff_bound_of_reductions {primitiveConstant supportConstant : ℝ} (hprimitive : 0 < primitiveConstant) (hsupport : 0 < supportConstant) : ∃ (outerConstant : ℝ), 0 < outerConstant ∧ ∀ (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (m : ℕ) (α β : Z4), 0 < ε → ε ≤ 1 / 4 → 1 ≤ |Real.log ε| → 1 ≤ m → PmCoeffMomentFubiniOutput M ρ lam ε m α β → WickAtSecondMomentLaw M ρ ε m → MomentUniformReductionOutputAt ρ lam ε m α β primitiveConstant supportConstant → RoutedMomentReductionOutput ρ lam ε m α β (lamEps lam ε ^ 2 * outerConstant * (primitiveConstant * lam) ^ (2 * m - 2)) → MeasureTheory.MemLp (pmCoeff M ρ lam ε m α β) 2 MeasureTheory.volume ∧ ∫ (ω : M.Ω), ‖pmCoeff M ρ lam ε m α β ω‖ ^ 2 ≤ deterministicMomentRHS outerConstant primitiveConstant lam ε m α β

Complete orderwise (3.24) closure from the entity-level R-324 interfaces.

The constants are chosen in the same order as in exists_deterministicMoment_bound_of_reductions. The only remaining mathematical premises are the two strictly upstream deterministic reduction outputs, the P-wick law, and the analytic Fubini output; no estimate is assumed at the random level.

theorem Anderson4D.deterministicMomentRHS_le_geometric_sq {outerConstant powerConstant lam ε : ℝ} {m : ℕ} {α β : Z4} (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hlam : 0 ≤ lam) (hm : 1 ≤ m) : deterministicMomentRHS outerConstant powerConstant lam ε m α β ≤ (‖↑(lamEps lam ε)‖ * √outerConstant * (powerConstant * lam) ^ (m - 1)) ^ 2

The deterministic right side of (3.24) is bounded by the square of its natural geometric L² scale. This is the normalization expected by the second-moment adapter in Main/GeometricTruncation.lean.

theorem Anderson4D.parametrix_coeff_geometric_second_moment_bound {M : NoiseModel} {ρ : SmoothCutoff} {outerConstant powerConstant lam ε : ℝ} {m : ℕ} {α β : Z4} (hfubini : PmCoeffMomentFubiniOutput M ρ lam ε m α β) (hwick : WickAtSecondMomentLaw M ρ ε m) (hdet : ‖deterministicMomentPairingSum ρ lam ε m α β‖ ≤ deterministicMomentRHS outerConstant powerConstant lam ε m α β) (houter : 0 ≤ outerConstant) (hpower : 0 ≤ powerConstant) (hlam : 0 ≤ lam) (hm : 1 ≤ m) : MeasureTheory.MemLp (pmCoeff M ρ lam ε m α β) 2 MeasureTheory.volume ∧ ∫ (ω : M.Ω), ‖pmCoeff M ρ lam ε m α β ω‖ ^ 2 ≤ (‖↑(lamEps lam ε)‖ * √outerConstant * (powerConstant * lam) ^ (m - 1)) ^ 2

Directly consumable squared form of (3.24). Taking K = sqrt outerConstant and q = powerConstant * lam gives exactly the premise shape of Prop36.tendsto_fullParametrixChar_of_geometric_second_moment_bound.