Summing the case-(3) parametrix identity

This module lifts the fixed-pairing case-(3) identity from IdentityAmbient to the exact finite prefix/tail sums in paper (3.18)--(3.19). The only hypotheses are the termwise integrability conditions needed by the displayed Bochner integral equalities. In particular, no identity or estimate is hidden in an abstract output predicate.

structure Anderson4D.PartialPairing.CaseThreeSummationIntegrability (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (q r : ℕ) (x y : T4) (ω : M.Ω) : Prop

The analytic regularity needed to sum all case-(3) identities at fixed prefix order 2(q+1) and tail order r.

The first two fields are precisely the hypotheses of caseThreeJointContribution_eq_randRI_add_delta; the last field licenses the finite-sum/integral exchange in the collapsed delta block.

• split (σ : PartialPairing (Fin (2 * (q + 1)))) (_hσ : IsNonSplit σ) (τ : PartialPairing (Fin r)) : NestedIntegrablePair3 paperMeasure paperMeasure (MeasureTheory.Measure.pi fun (x : Fin (2 * q + r)) => paperMeasure) (fun (z w : T4) (t : Fin (2 * q + r) → T4) => caseThreeAmbientCore M ρ ε q r σ τ x z w y ω t) fun (z w : T4) (t : Fin (2 * q + r) → T4) => caseThreeDiagonalCore M ρ ε q r σ τ x z w y ω t
• ambient (σ : PartialPairing (Fin (2 * (q + 1)))) (_hσ : IsNonSplit σ) (τ : PartialPairing (Fin r)) : MeasureTheory.Integrable (fun (v : Fin (2 * (q + 1) + r) → T4) => randIntegrand M ρ ε (σ.appendPairing τ) (assemble x y v) ω) (MeasureTheory.Measure.pi fun (x : Fin (2 * (q + 1) + r)) => paperMeasure)
• delta (σ : PartialPairing (Fin (2 * (q + 1)))) (_hσ : IsNonSplit σ) (τ : PartialPairing (Fin r)) : MeasureTheory.Integrable (fun (z : T4) => greenFn (x - z) * detJMass ρ lam ε (q + 1) σ * randRI M ρ lam ε r τ z y ω) paperMeasure

theorem Anderson4D.PartialPairing.sum_caseThreeFactorizedContribution_eq_randRI_add_delta (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (q r : ℕ) (x y : T4) (ω : M.Ω) (hint : CaseThreeSummationIntegrability M ρ lam ε q r x y ω) : ∑ σ : PartialPairing (Fin (2 * (q + 1))) with IsNonSplit σ, ∑ τ : PartialPairing (Fin r), caseThreeFactorizedContribution M ρ lam ε q r σ τ x y ω = ∑ σ : PartialPairing (Fin (2 * (q + 1))) with IsNonSplit σ, ∑ τ : PartialPairing (Fin r), randRI M ρ lam ε (2 * (q + 1) + r) (σ.appendPairing τ) x y ω + ∑ σ : PartialPairing (Fin (2 * (q + 1))) with IsNonSplit σ, ∑ τ : PartialPairing (Fin r), caseThreeDeltaContribution M ρ lam ε (q + 1) r σ τ x y ω

Summing the factorized case-(3) source over every non-split prefix and tail pairing gives the corresponding ambient random kernels plus all delta contributions, with multiplicity one.

theorem Anderson4D.PartialPairing.sum_caseThreeDeltaContribution_eq_countertermBlock (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (q r : ℕ) (x y : T4) (ω : M.Ω) (hint : CaseThreeSummationIntegrability M ρ lam ε q r x y ω) : ∑ σ : PartialPairing (Fin (2 * (q + 1))) with IsNonSplit σ, ∑ τ : PartialPairing (Fin r), caseThreeDeltaContribution M ρ lam ε (q + 1) r σ τ x y ω = caseThreeCountertermBlock M ρ lam ε (q + 1) r x y ω

The finite sum of the delta terms is exactly the already frozen counterterm block. This is the rigorous version of summing the C₂q,σ δ term in paper (3.19).

theorem Anderson4D.PartialPairing.sum_caseThreeFactorizedContribution_eq_randRI_add_counterterm (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (q r : ℕ) (x y : T4) (ω : M.Ω) (hint : CaseThreeSummationIntegrability M ρ lam ε q r x y ω) : ∑ σ : PartialPairing (Fin (2 * (q + 1))) with IsNonSplit σ, ∑ τ : PartialPairing (Fin r), caseThreeFactorizedContribution M ρ lam ε q r σ τ x y ω = ∑ σ : PartialPairing (Fin (2 * (q + 1))) with IsNonSplit σ, ∑ τ : PartialPairing (Fin r), randRI M ρ lam ε (2 * (q + 1) + r) (σ.appendPairing τ) x y ω + caseThreeCountertermBlock M ρ lam ε (q + 1) r x y ω

Fully collapsed fixed-order case-(3) sum: the source block is the ambient appended-pairing sum plus C₂(q+1) Pᵣ under the free Green convolution.