Haar reindexing for the proper R-324 convolution

The proper cross-block estimate contains two surviving inverse-square connector edges and one translation-invariant inserted kernel. This file performs the exact product-Haar shear that exposes the binary convolution of the two connector edges. No inequality is used here.

noncomputable def Anderson4D.r324KernelTriple (q : T4 → ℝ) (u v : T4) (p : T4 × T4) : ℝ

Product-space integrand with a generic kernel on the endpoint difference.

Equations

• Anderson4D.r324KernelTriple q u v p = Anderson4D.invSqKer (u - p.1) * q (p.1 - p.2) * Anderson4D.invSqKer (p.2 - v)

theorem Anderson4D.measurePreserving_r324KernelTripleShear (v : T4) : MeasureTheory.MeasurePreserving (⇑(Anderson4D.r324KernelTripleShearMeasurableEquiv✝ v)) (paperMeasure.prod paperMeasure) (paperMeasure.prod paperMeasure)

The affine shear (h,z) ↦ (h+z+v,z+v) preserves product Haar measure. In these coordinates h is the inserted endpoint difference and z is the right connector displacement.

theorem Anderson4D.r324KernelTriple_shear (q : T4 → ℝ) (u v h z : T4) : r324KernelTriple q u v (h + (z + v), z + v) = q h * (invSqKer (u - v - h - z) * invSqKer z)

theorem Anderson4D.integrable_r324KernelTriple_shear (q : T4 → ℝ) (u v : T4) (hint : MeasureTheory.Integrable (r324KernelTriple q u v) (paperMeasure.prod paperMeasure)) : MeasureTheory.Integrable (fun (p : T4 × T4) => r324KernelTriple q u v (p.1 + (p.2 + v), p.2 + v)) (paperMeasure.prod paperMeasure)

theorem Anderson4D.integral_r324KernelTriple_eq_sheared (q : T4 → ℝ) (u v : T4) : ∫ (p : T4 × T4), r324KernelTriple q u v p ∂paperMeasure.prod paperMeasure = ∫ (p : T4 × T4), r324KernelTriple q u v (p.1 + (p.2 + v), p.2 + v) ∂paperMeasure.prod paperMeasure

theorem Anderson4D.integral_r324KernelTriple_sheared_eq_iterated (q : T4 → ℝ) (u v : T4) (hint : MeasureTheory.Integrable (r324KernelTriple q u v) (paperMeasure.prod paperMeasure)) : ∫ (p : T4 × T4), r324KernelTriple q u v (p.1 + (p.2 + v), p.2 + v) ∂paperMeasure.prod paperMeasure = ∫ (h : T4), ∫ (z : T4), r324KernelTriple q u v (h + (z + v), z + v) ∂paperMeasure ∂paperMeasure

theorem Anderson4D.integral_r324KernelTriple_shear_section_eq_weightedBinary (q : T4 → ℝ) (u v h : T4) : ∫ (z : T4), r324KernelTriple q u v (h + (z + v), z + v) ∂paperMeasure = q h * ∫ (z : T4), invSqKer (u - v - h - z) * invSqKer z ∂paperMeasure

theorem Anderson4D.integrable_r324KernelTriple_weightedBinary (q : T4 → ℝ) (u v : T4) (hint : MeasureTheory.Integrable (r324KernelTriple q u v) (paperMeasure.prod paperMeasure)) : MeasureTheory.Integrable (fun (h : T4) => q h * ∫ (z : T4), invSqKer (u - v - h - z) * invSqKer z ∂paperMeasure) paperMeasure

theorem Anderson4D.integral_r324KernelTriple_iterated_eq_weightedBinary (q : T4 → ℝ) (u v : T4) : ∫ (h : T4), ∫ (z : T4), r324KernelTriple q u v (h + (z + v), z + v) ∂paperMeasure ∂paperMeasure = ∫ (h : T4), q h * ∫ (z : T4), invSqKer (u - v - h - z) * invSqKer z ∂paperMeasure ∂paperMeasure

theorem Anderson4D.integral_r324KernelTriple_eq_weightedBinary (q : T4 → ℝ) (u v : T4) (hint : MeasureTheory.Integrable (r324KernelTriple q u v) (paperMeasure.prod paperMeasure)) : ∫ (p : T4 × T4), r324KernelTriple q u v p ∂paperMeasure.prod paperMeasure = ∫ (h : T4), q h * ∫ (z : T4), invSqKer (u - v - h - z) * invSqKer z ∂paperMeasure ∂paperMeasure

Exact Fubini form after the product-Haar shear. The right-hand side is the inserted kernel averaged against the binary inverse-square convolution at u-v-h.