Global analytic closure for the parametrix identity

The algebraic proof of Proposition 3.4 keeps every use of Fubini in an explicit fixed-endpoint ledger. Those ledgers are not extra hypotheses: after integrating both external endpoints, the random pairing profiles are jointly integrable. This file converts that global fact into the almost-everywhere endpoint statements needed by the identity proof.

The endpoint diagonal remains exceptional, as it must in four dimensions.

theorem Anderson4D.PartialPairing.integrable_headTailVariables (n : ℕ) (f : (Fin (n + 1) → T4) → ℝ) (hf : MeasureTheory.Integrable f (MeasureTheory.Measure.pi fun (x : Fin (n + 1)) => paperMeasure)) : MeasureTheory.Integrable (fun (p : T4 × (Fin n → T4)) => f (Fin.cons p.1 p.2)) (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin n) => paperMeasure))

Separating the new head variable from the old internal variables preserves integrability.

theorem Anderson4D.PartialPairing.integrable_caseThreeVariables (q r : ℕ) (f : (Fin (2 * (q + 1) + r) → T4) → ℝ) (hf : MeasureTheory.Integrable f (MeasureTheory.Measure.pi fun (x : Fin (2 * (q + 1) + r)) => paperMeasure)) : MeasureTheory.Integrable (fun (p : T4 × T4 × (Fin (2 * q + r) → T4)) => f (caseThreeAmbientInternal q r p.1 p.2.1 p.2.2)) (paperMeasure.prod (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin (2 * q + r)) => paperMeasure)))

The paper-order case-(3) variables may be rearranged into (z,w,remaining) without changing integrability.

theorem Anderson4D.PartialPairing.integrable_caseThreeContractionVariables (q r : ℕ) (f : (Fin (2 * q + 1 + r) → T4) → ℝ) (hf : MeasureTheory.Integrable f (MeasureTheory.Measure.pi fun (x : Fin (2 * q + 1 + r)) => paperMeasure)) : MeasureTheory.Integrable (fun (p : T4 × (Fin (2 * q + r) → T4)) => f (caseThreeContractionInternal q r p.1 p.2)) (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin (2 * q + r)) => paperMeasure))

The old variables of an actual case-(3) contraction may be rearranged into the closed-prefix endpoint and the remaining variables.

theorem Anderson4D.PartialPairing.integrable_outer_caseThreeContractionVariables (q r : ℕ) (f : T4 → (Fin (2 * q + 1 + r) → T4) → ℝ) (hf : MeasureTheory.Integrable (fun (p : T4 × (Fin (2 * q + 1 + r) → T4)) => f p.1 p.2) (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin (2 * q + 1 + r)) => paperMeasure))) : MeasureTheory.Integrable (fun (p : T4 × T4 × (Fin (2 * q + r) → T4)) => f p.1 (caseThreeContractionInternal q r p.2.1 p.2.2)) (paperMeasure.prod (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin (2 * q + r)) => paperMeasure)))

The preceding contraction-variable permutation may be performed under an additional outer variable.

theorem Anderson4D.PartialPairing.nestedIntegrablePair3_of_joint {k : ℕ} {left right : T4 → T4 → (Fin k → T4) → ℝ} (hleft : MeasureTheory.Integrable (fun (p : T4 × T4 × (Fin k → T4)) => left p.1 p.2.1 p.2.2) (paperMeasure.prod (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin k) => paperMeasure)))) (hright : MeasureTheory.Integrable (fun (p : T4 × T4 × (Fin k → T4)) => right p.1 p.2.1 p.2.2) (paperMeasure.prod (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin k) => paperMeasure)))) : NestedIntegrablePair3 paperMeasure paperMeasure (MeasureTheory.Measure.pi fun (x : Fin k) => paperMeasure) left right

Fully joint integrability of two three-variable kernels supplies the six nested conditions used by integral3_add.

theorem Anderson4D.PartialPairing.integrable_leftCreationWeightedCore (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (n : ℕ) (κ : PartialPairing (Fin n)) (x y : T4) (ω : M.Ω) (hnew : MeasureTheory.Integrable (fun (u : Fin (n + 1) → T4) => randIntegrand M ρ ε ((wickHeadEquiv n) (Sum.inl κ)) (assemble x y u) ω) (MeasureTheory.Measure.pi fun (x : Fin (n + 1)) => paperMeasure)) : MeasureTheory.Integrable (fun (p : T4 × (Fin n → T4)) => leftCreationWeightedCore M ρ ε κ x p.1 y p.2 ω) (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin n) => paperMeasure))

Joint integrability of a created Wick term follows from the global integrability of the corresponding head-single random profile.

theorem Anderson4D.PartialPairing.leftPairingSplitIntegrability_of_joint (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) (n : ℕ) (κ : PartialPairing (Fin n)) (x y : T4) (ω : M.Ω) (hcreation : MeasureTheory.Integrable (fun (p : T4 × (Fin n → T4)) => leftCreationWeightedCore M ρ ε κ x p.1 y p.2 ω) (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin n) => paperMeasure))) (hcontraction : ∀ (j : Fin κ.singles.card), MeasureTheory.Integrable (fun (p : T4 × (Fin n → T4)) => leftRankedContractionWeightedCore M ρ ε κ j x p.1 y p.2 ω) (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin n) => paperMeasure))) : LeftPairingSplitIntegrability M ρ ε n κ x y ω

A genuinely joint (new head, old variables) integrability statement discharges all four nested-Fubini fields of the Wick split ledger.

theorem Anderson4D.PartialPairing.integrable_leftRankedContraction_flat (M : NoiseModel) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (n : ℕ) (κ : PartialPairing (Fin n)) (j : Fin κ.singles.card) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) : MeasureTheory.Integrable (fun (p : PairingHalfPhysicalPoint (n + 1)) => ↑(leftRankedContractionWeightedCore M ρ ε κ j p.1 (p.2.2 0) p.2.1 (Fin.tail p.2.2) ω)) (pairingHalfPhysicalMeasure (n + 1))

Each individual Wick-contraction term is jointly integrable in both endpoints and all old internal variables. Its deterministic factor is the head-single profile; the covariance and the Wick polynomial form a bounded measurable multiplier on a continuous noise sample.

Free Green convolution of one pairing profile

def Anderson4D.PartialPairing.pairingDropHeadPhysicalMap (r : ℕ) : PairingHalfPhysicalPoint (r + 1) → PairingHalfPhysicalPoint r

Drop the first internal variable of an order-r+1 physical tuple and use it as the left endpoint of an order-r tuple.

Equations

• Anderson4D.PartialPairing.pairingDropHeadPhysicalMap r p = (p.2.2 0, p.2.1, Fin.tail p.2.2)

theorem Anderson4D.PartialPairing.measurable_pairingDropHeadPhysicalMap (r : ℕ) : Measurable (pairingDropHeadPhysicalMap r)

theorem Anderson4D.PartialPairing.integrable_green_mul_randIntegrand_flat (M : NoiseModel) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (r : ℕ) (τ : PartialPairing (Fin r)) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) : MeasureTheory.Integrable (fun (p : PairingHalfPhysicalPoint (r + 1)) => ↑(greenFn (p.1 - p.2.2 0)) * ↑(randIntegrand M ρ ε τ (assemble (p.2.2 0) p.2.1 (Fin.tail p.2.2)) ω)) (pairingHalfPhysicalMeasure (r + 1))

Before integrating the new head variable, a free Green convolution of one random pairing profile is jointly integrable in all spatial variables.

theorem Anderson4D.PartialPairing.ae_ae_integrable_green_mul_randRI (M : NoiseModel) (ρ : SmoothCutoff) (lam : ℝ) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (r : ℕ) (τ : PartialPairing (Fin r)) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) : ∀ᵐ (x : T4) (y : T4) ∂paperMeasure, MeasureTheory.Integrable (fun (z : T4) => greenFn (x - z) * randRI M ρ lam ε r τ z y ω) paperMeasure

Consequently the free Green convolution of randRI is integrable for almost every endpoint pair.

theorem Anderson4D.PartialPairing.ae_ae_integrable_leftRankedContractionWeightedCore (M : NoiseModel) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (n : ℕ) (κ : PartialPairing (Fin n)) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) : ∀ᵐ (x : T4) (y : T4) ∂paperMeasure, ∀ (j : Fin κ.singles.card), MeasureTheory.Integrable (fun (p : T4 × (Fin n → T4)) => leftRankedContractionWeightedCore M ρ ε κ j x p.1 y p.2 ω) (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin n) => paperMeasure))

The contraction terms in the fixed-endpoint Wick split are jointly integrable for almost every endpoint pair, simultaneously over the finite set of Wick ranks.

theorem Anderson4D.PartialPairing.ae_ae_leftPairingSplitIntegrability (M : NoiseModel) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (n : ℕ) (κ : PartialPairing (Fin n)) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) : ∀ᵐ (x : T4) (y : T4) ∂paperMeasure, LeftPairingSplitIntegrability M ρ ε n κ x y ω

The complete Wick-split ledger is automatic for almost every endpoint pair on every continuous mollified-noise sample.

theorem Anderson4D.PartialPairing.integrable_leftPairingOuter_of_split (M : NoiseModel) (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (κ : PartialPairing (Fin n)) (x y : T4) (ω : M.Ω) (hint : LeftPairingSplitIntegrability M ρ ε n κ x y ω) : MeasureTheory.Integrable (fun (z : T4) => greenFn (x - z) * (M.xiEps ρ ε ω z * randRI M ρ lam ε n κ z y ω)) paperMeasure

The integrability of one outer noise--pairing convolution follows from the already constructed Wick-split ledger.

theorem Anderson4D.PartialPairing.ae_ae_leftOrderSourceIntegrability (M : NoiseModel) (ρ : SmoothCutoff) (lam : ℝ) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (n : ℕ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) : ∀ᵐ (x : T4) (y : T4) ∂paperMeasure, LeftOrderSourceIntegrability M ρ lam ε n x y ω

The paper-facing outer noise source ledger holds almost everywhere, simultaneously over the finite family of old partial pairings.

Marked contractions and the case-(3) head ledger

noncomputable def Anderson4D.PartialPairing.leftMarkedContractionWeightedCore (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) {n : ℕ} (d : MarkedSingle (Fin n)) (x z y : T4) (v : Fin n → T4) (ω : M.Ω) : ℝ

The weighted contraction core indexed directly by a marked old single.

Equations

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

theorem Anderson4D.PartialPairing.leftRankedContractionWeightedCore_eq_marked (M : NoiseModel) (ρ : SmoothCutoff) (ε : ℝ) {n : ℕ} (κ : PartialPairing (Fin n)) (j : Fin κ.singles.card) (x z y : T4) (v : Fin n → T4) (ω : M.Ω) : leftRankedContractionWeightedCore M ρ ε κ j x z y v ω = leftMarkedContractionWeightedCore M ρ ε ((rankedSingleEquiv (Fin n)) ⟨κ, j⟩) x z y v ω

Rank indexing and marked-single indexing give the same unintegrated weighted contraction core.

theorem Anderson4D.PartialPairing.ae_ae_integrable_leftMarkedContractionWeightedCore (M : NoiseModel) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {n : ℕ} (d : MarkedSingle (Fin n)) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) : ∀ᵐ (x : T4) (y : T4) ∂paperMeasure, MeasureTheory.Integrable (fun (p : T4 × (Fin n → T4)) => leftMarkedContractionWeightedCore M ρ ε d x p.1 y p.2 ω) (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin n) => paperMeasure))

Every directly marked contraction has the same almost-everywhere joint integrability as its ranked presentation.

theorem Anderson4D.PartialPairing.ae_ae_caseThreeHeadContractionIntegrability (M : NoiseModel) (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (q r : ℕ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) : ∀ᵐ (x : T4) (y : T4) ∂paperMeasure, CaseThreeHeadContractionIntegrability M ρ ε q r x y ω

The head-contraction ledger used in paper case (3) is an automatic specialization of marked-contraction integrability.

Automatic closure of the case-(3) summation ledger

theorem Anderson4D.PartialPairing.ae_ae_caseThreeSummationIntegrability_fixed (M : NoiseModel) (ρ : SmoothCutoff) (lam : ℝ) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (q r : ℕ) (σ : PartialPairing (Fin (2 * (q + 1)))) (τ : PartialPairing (Fin r)) (hσ : IsNonSplit σ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) : ∀ᵐ (x : T4) (y : T4) ∂paperMeasure, (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) ∧ 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) ∧ MeasureTheory.Integrable (fun (z : T4) => greenFn (x - z) * detJMass ρ lam ε (q + 1) σ * randRI M ρ lam ε r τ z y ω) paperMeasure

For one fixed non-split prefix and one fixed tail pairing, all three analytic fields used by the case-(3) summation are automatic almost everywhere in the external endpoints.

theorem Anderson4D.PartialPairing.ae_ae_caseThreeSummationIntegrability (M : NoiseModel) (ρ : SmoothCutoff) (lam : ℝ) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (q r : ℕ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) : ∀ᵐ (x : T4) (y : T4) ∂paperMeasure, CaseThreeSummationIntegrability M ρ lam ε q r x y ω

The complete finite case-(3) summation ledger is automatic almost everywhere in the external endpoints.

theorem Anderson4D.PartialPairing.ae_ae_leftWithPrefixCaseThreeIntegrability (M : NoiseModel) (ρ : SmoothCutoff) (lam : ℝ) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (n : ℕ) (ω : M.Ω) (hξ : Continuous (M.xiEps ρ ε ω)) : ∀ᵐ (x : T4) (y : T4) ∂paperMeasure, LeftWithPrefixCaseThreeIntegrability M ρ lam ε n x y ω

All minimal-prefix case-(3) ledgers at one old order hold simultaneously almost everywhere.