Joint integrability of the R-324 deterministic contractions

This file expands the renormalized Green differences in the two copies of (4.18). Choosing either the original edge or its shortcut at every extracted right endpoint produces an increasing Green tree, so the analytic result of R324TreeIntegrability.lean applies term by term.

Extracted right edges and their shortcut parents

theorem Anderson4D.exists_extractedPairOfRightEdge {m : ℕ} (κ : PartialPairing (Fin m)) (i : Fin (m + 1)) (hi : i ∈ extractedRightEdges κ) : ∃ p ∈ extract κ, extractedRightEdge p = i

Membership in extractedRightEdges carries an actual extracted interval with that right edge.

noncomputable def Anderson4D.extractedPairOfRightEdge {m : ℕ} (κ : PartialPairing (Fin m)) (i : Fin (m + 1)) (hi : i ∈ extractedRightEdges κ) : Fin m × Fin m

The unique extracted interval whose replaced right edge is i.

Equations

• Anderson4D.extractedPairOfRightEdge κ i hi = Classical.choose ⋯

theorem Anderson4D.extractedPairOfRightEdge_mem {m : ℕ} (κ : PartialPairing (Fin m)) (i : Fin (m + 1)) (hi : i ∈ extractedRightEdges κ) : extractedPairOfRightEdge κ i hi ∈ extract κ

theorem Anderson4D.extractedRightEdge_extractedPairOfRightEdge {m : ℕ} (κ : PartialPairing (Fin m)) (i : Fin (m + 1)) (hi : i ∈ extractedRightEdges κ) : extractedRightEdge (extractedPairOfRightEdge κ i hi) = i

def Anderson4D.ordinaryEdgeParent {m : ℕ} (i : Fin (m + 1)) : Fin (↑i + 1)

The predecessor of an ordinary chain edge, in dependent parent form.

Equations

• Anderson4D.ordinaryEdgeParent i = ⟨↑i, ⋯⟩

noncomputable def Anderson4D.extractedShortcutParent {m : ℕ} (κ : PartialPairing (Fin m)) (i : Fin (m + 1)) (hi : i ∈ extractedRightEdges κ) : Fin (↑i + 1)

The earlier endpoint of the shortcut replacing an extracted right edge.

Equations

• Anderson4D.extractedShortcutParent κ i hi = ⟨↑(Anderson4D.extractedPairOfRightEdge κ i hi).1 + 1, ⋯⟩

noncomputable def Anderson4D.expandedGreenTreeParent {m : ℕ} (κ : PartialPairing (Fin m)) (original : Finset (Fin (m + 1))) : IncreasingTreeParent (m + 1)

Parent map of one fully expanded renormalized Green summand. Membership in original means that the original chain edge is chosen; otherwise the shortcut is chosen when it exists.

Equations

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

noncomputable def Anderson4D.originalGreenEdge {m : ℕ} (x : Fin (m + 2) → T4) (i : Fin (m + 1)) : ℂ

Original Green edge with right endpoint i+1.

Equations

• Anderson4D.originalGreenEdge x i = ↑(Anderson4D.greenFn (x i.castSucc - x i.succ))

@[simp]

theorem Anderson4D.extractedRightEdge_castSucc {m : ℕ} (p : Fin m × Fin m) : (extractedRightEdge p).castSucc = varIdx p.2

@[simp]

theorem Anderson4D.extractedRightEdge_succ {m : ℕ} (p : Fin m × Fin m) : (extractedRightEdge p).succ = ⟨↑p.2 + 2, ⋯⟩

noncomputable def Anderson4D.extractedShortcutGreenEdge {m : ℕ} (κ : PartialPairing (Fin m)) (x : Fin (m + 2) → T4) (i : Fin (m + 1)) : ℂ

Shortcut Green edge at an extracted right endpoint, and zero at an unextracted endpoint. The zero makes the product-of-sums expansion uniform over all edges.

Equations

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

noncomputable def Anderson4D.expandedGreenBranch {m : ℕ} (κ : PartialPairing (Fin m)) (original : Finset (Fin (m + 1))) (x : Fin (m + 2) → T4) : ℂ

One term in the powerset expansion of the product of edge sums.

Equations

• Anderson4D.expandedGreenBranch κ original x = (∏ i ∈ original, Anderson4D.originalGreenEdge x i) * ∏ i ∈ originalᶜ, Anderson4D.extractedShortcutGreenEdge κ x i

theorem Anderson4D.expandedGreenBranch_eq_tree {m : ℕ} (κ : PartialPairing (Fin m)) (original : Finset (Fin (m + 1))) (hshortcut : ∀ i ∉ original, i ∈ extractedRightEdges κ) : expandedGreenBranch κ original = increasingTreeGreenProduct (expandedGreenTreeParent κ original)

If every chosen shortcut really is extracted, the corresponding branch is exactly the increasing-tree Green product.

theorem Anderson4D.integrable_expandedGreenBranch {m : ℕ} (κ : PartialPairing (Fin m)) (original : Finset (Fin (m + 1))) : MeasureTheory.Integrable (expandedGreenBranch κ original) (MeasureTheory.Measure.pi fun (x : Fin (m + 2)) => paperMeasure)

Every branch in the uniform powerset expansion is jointly integrable. Branches selecting a nonexistent shortcut vanish; all other branches are increasing Green trees.

noncomputable def Anderson4D.expandedGreenMajorant {m : ℕ} (κ : PartialPairing (Fin m)) (x : Fin (m + 2) → T4) : ℂ

Nonnegative complex majorant obtained by replacing every extracted difference by the sum of its two Green terms.

Equations

• Anderson4D.expandedGreenMajorant κ x = ∏ i : Fin (m + 1), (Anderson4D.originalGreenEdge x i + Anderson4D.extractedShortcutGreenEdge κ x i)

theorem Anderson4D.expandedGreenMajorant_eq_sum_branches {m : ℕ} (κ : PartialPairing (Fin m)) : expandedGreenMajorant κ = fun (x : Fin (m + 2) → T4) => ∑ original : Finset (Fin (m + 1)), expandedGreenBranch κ original x

The edgewise majorant is a finite sum of the integrable expanded-tree branches.

theorem Anderson4D.integrable_expandedGreenMajorant {m : ℕ} (κ : PartialPairing (Fin m)) : MeasureTheory.Integrable (expandedGreenMajorant κ) (MeasureTheory.Measure.pi fun (x : Fin (m + 2)) => paperMeasure)

Joint integrability of the complete Green edge majorant.

Comparison with the renormalized Green skeleton

noncomputable def Anderson4D.renormalizedGreenSkeleton {m : ℕ} (κ : PartialPairing (Fin m)) (x : Fin (m + 2) → T4) : ℂ

The Green-only part of detIntegrand, before the bounded covariance product is attached.

Equations

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

theorem Anderson4D.extract_nodup {m : ℕ} (κ : PartialPairing (Fin m)) : (extract κ).Nodup

Distinct extracted right endpoints make the extraction list itself duplicate-free.

theorem Anderson4D.extractedRightEdge_injective_on_extract {m : ℕ} (κ : PartialPairing (Fin m)) {p q : Fin m × Fin m} (hp : p ∈ extract κ) (hq : q ∈ extract κ) (hedge : extractedRightEdge p = extractedRightEdge q) : p = q

Two extracted intervals with the same replaced right edge coincide.

theorem Anderson4D.extractedRightEdge_mem_extractedRightEdges {m : ℕ} (κ : PartialPairing (Fin m)) (p : Fin m × Fin m) (hp : p ∈ extract κ) : extractedRightEdge p ∈ extractedRightEdges κ

Every extracted interval contributes its right edge to the replacement finset.

theorem Anderson4D.extractedPairOfRightEdge_eq {m : ℕ} (κ : PartialPairing (Fin m)) (p : Fin m × Fin m) (hp : p ∈ extract κ) : extractedPairOfRightEdge κ (extractedRightEdge p) ⋯ = p

The chosen inverse of an extracted right edge returns the original interval.

theorem Anderson4D.prod_extractedRightEdges_eq_extract_prod {m : ℕ} {M : Type u_1} [CommMonoid M] (κ : PartialPairing (Fin m)) (f : Fin (m + 1) → M) : ∏ i ∈ extractedRightEdges κ, f i = (List.map (fun (p : Fin m × Fin m) => f (extractedRightEdge p)) (extract κ)).prod

Reindex a product over the extracted right-edge finset by the original extraction list.

@[simp]

theorem Anderson4D.extractedShortcutGreenEdge_extractedRightEdge {m : ℕ} (κ : PartialPairing (Fin m)) (p : Fin m × Fin m) (hp : p ∈ extract κ) (x : Fin (m + 2) → T4) : extractedShortcutGreenEdge κ x (extractedRightEdge p) = ↑(greenFn (x (varIdx p.1) - x (extractedRightEdge p).succ))

noncomputable def Anderson4D.expandedGreenDifferenceProduct {m : ℕ} (κ : PartialPairing (Fin m)) (x : Fin (m + 2) → T4) : ℂ

The uniform edge product with subtraction. Unextracted shortcut terms are zero, while extracted ones reproduce the renormalized differences.

Equations

• Anderson4D.expandedGreenDifferenceProduct κ x = ∏ i : Fin (m + 1), (Anderson4D.originalGreenEdge x i - Anderson4D.extractedShortcutGreenEdge κ x i)

theorem Anderson4D.renormalizedGreenSkeleton_eq_differenceProduct {m : ℕ} (κ : PartialPairing (Fin m)) : renormalizedGreenSkeleton κ = expandedGreenDifferenceProduct κ

The Green skeleton in the closed renormalized integrand is exactly the uniform edge-difference product.

theorem Anderson4D.measurable_originalGreenEdge {m : ℕ} (i : Fin (m + 1)) : Measurable fun (x : Fin (m + 2) → T4) => originalGreenEdge x i

theorem Anderson4D.measurable_extractedShortcutGreenEdge {m : ℕ} (κ : PartialPairing (Fin m)) (i : Fin (m + 1)) : Measurable fun (x : Fin (m + 2) → T4) => extractedShortcutGreenEdge κ x i

theorem Anderson4D.measurable_expandedGreenDifferenceProduct {m : ℕ} (κ : PartialPairing (Fin m)) : Measurable (expandedGreenDifferenceProduct κ)

theorem Anderson4D.norm_expandedGreenDifferenceProduct_le {m : ℕ} (κ : PartialPairing (Fin m)) (x : Fin (m + 2) → T4) : ‖expandedGreenDifferenceProduct κ x‖ ≤ ‖expandedGreenMajorant κ x‖

Edgewise triangle inequality between the signed renormalized expansion and its nonnegative product-of-sums majorant.

theorem Anderson4D.integrable_renormalizedGreenSkeleton {m : ℕ} (κ : PartialPairing (Fin m)) : MeasureTheory.Integrable (renormalizedGreenSkeleton κ) (MeasureTheory.Measure.pi fun (x : Fin (m + 2)) => paperMeasure)

Joint integrability of the signed renormalized Green skeleton.

Bounded covariance factor and the full deterministic integrand

noncomputable def Anderson4D.detCovarianceFactor (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (κ : PartialPairing (Fin m)) (x : Fin (m + 2) → T4) : ℂ

Covariance part of one deterministic closed integrand, coerced to the same complex scalar field as the Green skeleton.

Equations

• Anderson4D.detCovarianceFactor ρ ε κ x = ↑(∏ i ∈ κ.pairSupport with i < κ i, ρ.etaEpsT4 ε (x (Anderson4D.varIdx i) - x (Anderson4D.varIdx (κ i))))

theorem Anderson4D.measurable_detCovarianceFactor (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (κ : PartialPairing (Fin m)) : Measurable (detCovarianceFactor ρ ε κ)

theorem Anderson4D.exists_norm_detCovarianceFactor_le (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} (κ : PartialPairing (Fin m)) : ∃ (B : ℝ), 0 ≤ B ∧ ∀ (x : Fin (m + 2) → T4), ‖detCovarianceFactor ρ ε κ x‖ ≤ B

At a positive small scale the covariance product is uniformly bounded on the compact physical product space.

theorem Anderson4D.detIntegrand_eq_renormalizedGreenSkeleton_mul_covariance (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (κ : PartialPairing (Fin m)) (x : Fin (m + 2) → T4) : ↑(detIntegrand ρ ε m κ x) = renormalizedGreenSkeleton κ x * detCovarianceFactor ρ ε κ x

Exact factorization of the frozen deterministic integrand into its signed Green skeleton and bounded covariance product.

theorem Anderson4D.integrable_detIntegrand_joint (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} (κ : PartialPairing (Fin m)) : MeasureTheory.Integrable (fun (x : Fin (m + 2) → T4) => ↑(detIntegrand ρ ε m κ x)) (MeasureTheory.Measure.pi fun (x : Fin (m + 2)) => paperMeasure)

Joint integrability of every deterministic closed-form parametrix integrand in all of its m+2 spatial vertices.

Flat and doubled physical coordinates

noncomputable def Anderson4D.r324FlatAssembleMeasurableEquiv (m : ℕ) : (Fin (m + 2) → T4) ≃ᵐ T4 × T4 × (Fin m → T4)

Split the first and last coordinates of a complete parametrix tuple. Its inverse is exactly assemble.

Equations

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

@[simp]

theorem Anderson4D.r324FlatAssembleMeasurableEquiv_symm_apply (m : ℕ) (x y : T4) (v : Fin m → T4) : (r324FlatAssembleMeasurableEquiv m).symm (x, y, v) = assemble x y v

theorem Anderson4D.measurePreserving_r324FlatAssembleMeasurableEquiv (m : ℕ) : MeasureTheory.MeasurePreserving (⇑(r324FlatAssembleMeasurableEquiv m)) (MeasureTheory.Measure.pi fun (x : Fin (m + 2)) => paperMeasure) (paperMeasure.prod (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin m) => paperMeasure)))

The complete-tuple/flat-coordinate split preserves the paper's Haar product measures.

theorem Anderson4D.integrable_detIntegrand_flat (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} (κ : PartialPairing (Fin m)) : MeasureTheory.Integrable (fun (p : T4 × T4 × (Fin m → T4)) => ↑(detIntegrand ρ ε m κ (assemble p.1 p.2.1 p.2.2))) (paperMeasure.prod (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin m) => paperMeasure)))

Joint integrability in the paper's flat (x,y,v) coordinates.

def Anderson4D.r324MoveMiddleMeasurableEquiv (A : Type u_1) (B : Type u_2) (C : Type u_3) [MeasurableSpace A] [MeasurableSpace B] [MeasurableSpace C] : A × B × C ≃ᵐ B × A × C

Move the middle coordinate of a triple to the front. This small equivalence is used twice to regroup the doubled physical variables without asserting any pointwise Fubini statement.

Equations

• Anderson4D.r324MoveMiddleMeasurableEquiv A B C = MeasurableEquiv.prodAssoc.symm.trans ((MeasurableEquiv.prodComm.prodCongr (MeasurableEquiv.refl C)).trans MeasurableEquiv.prodAssoc)

theorem Anderson4D.measurePreserving_r324MoveMiddleMeasurableEquiv {A : Type u_1} {B : Type u_2} {C : Type u_3} [MeasurableSpace A] [MeasurableSpace B] [MeasurableSpace C] (μ : MeasureTheory.Measure A) (ν : MeasureTheory.Measure B) (τ : MeasureTheory.Measure C) [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] [MeasureTheory.SFinite τ] : MeasureTheory.MeasurePreserving (⇑(r324MoveMiddleMeasurableEquiv A B C)) (μ.prod (ν.prod τ)) (ν.prod (μ.prod τ))

noncomputable def Anderson4D.r324DoublePiMeasurableEquiv (m : ℕ) : (Fin (2 * m) → T4) ≃ᵐ (Fin m → T4) × (Fin m → T4)

Split a doubled tuple according to its left and right moment labels.

Equations

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

@[simp]

theorem Anderson4D.r324DoublePiMeasurableEquiv_apply (m : ℕ) (v : Fin (2 * m) → T4) : (r324DoublePiMeasurableEquiv m) v = (fun (i : Fin m) => v (leftMomentIndex i), fun (j : Fin m) => v (rightMomentIndex j))

theorem Anderson4D.measurePreserving_r324DoublePiMeasurableEquiv (m : ℕ) : MeasureTheory.MeasurePreserving (⇑(r324DoublePiMeasurableEquiv m)) (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))

noncomputable def Anderson4D.r324PhysicalSplitMeasurableEquiv (m : ℕ) : R324PhysicalPoint m ≃ᵐ (T4 × T4 × (Fin m → T4)) × T4 × T4 × (Fin m → T4)

Regroup (x,y,z,w,v⁺⊔v⁻) into the two independent flat parametrix tuples (x,y,v⁺) and (z,w,v⁻).

Equations

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

@[simp]

theorem Anderson4D.r324PhysicalSplitMeasurableEquiv_apply (m : ℕ) (p : R324PhysicalPoint m) : (r324PhysicalSplitMeasurableEquiv m) p = ((p.1, p.2.1, fun (i : Fin m) => p.2.2.2.2 (leftMomentIndex i)), p.2.2.1, p.2.2.2.1, fun (i : Fin m) => p.2.2.2.2 (rightMomentIndex i))

theorem Anderson4D.measurePreserving_r324PhysicalSplitMeasurableEquiv (m : ℕ) : MeasureTheory.MeasurePreserving (⇑(r324PhysicalSplitMeasurableEquiv m)) (r324PhysicalMeasure m) ((paperMeasure.prod (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin m) => paperMeasure))).prod (paperMeasure.prod (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin m) => paperMeasure))))

The physical regrouping preserves the genuine five-group product measure.

theorem Anderson4D.integrable_r324Flatten_detIntegrand_product (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} (κp κm : PartialPairing (Fin m)) : MeasureTheory.Integrable (r324Flatten fun (x y z w : T4) (v : Fin (2 * m) → T4) => ↑(detIntegrand ρ ε m κp (assemble x y fun (i : Fin m) => v (leftMomentIndex i)) * detIntegrand ρ ε m κm (assemble z w fun (i : Fin m) => v (rightMomentIndex i)))) (r324PhysicalMeasure m)

Joint integrability of the bare doubled deterministic profile before the four Fourier characters and the cross-covariance factors are attached.

The full deterministic moment contraction

theorem Anderson4D.measurable_momentCrossCovarianceProduct (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : Measurable (momentCrossCovarianceProduct ρ ε m κp κm π)

The cross-copy covariance product is measurable in the doubled internal tuple.

theorem Anderson4D.exists_norm_momentCrossCovarianceProduct_le (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : ∃ (B : ℝ), 0 ≤ B ∧ ∀ (v : Fin (2 * m) → T4), ‖↑(momentCrossCovarianceProduct ρ ε m κp κm π v)‖ ≤ B

At positive scale, every cross-copy covariance product is uniformly bounded. The bound may depend on the frozen pairing data and scale, which is all that joint integrability requires.

theorem Anderson4D.integrable_r324Flatten_deterministicMomentIntegrand (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} (α β : Z4) (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : MeasureTheory.Integrable (r324Flatten (deterministicMomentIntegrand ρ ε m α β κp κm π)) (r324PhysicalMeasure m)

Every contraction term in the deterministic form of (3.24)/(4.18) is jointly integrable on its genuine product space.

theorem Anderson4D.r324MomentIntegrable_all (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} (α β : Z4) (e : MomentContraction m) : R324MomentIntegrable ρ ε m α β e

Uniformly package the preceding theorem as the physical-fiber integrability ledger consumed by deterministic R-324 reduction.