Gap-first coordinates for an incoming R-324 head

The primitive-block coordinate split used by the signed R-324 reduction first exposes the ordered endpoint pair (first, last). The exceptional Fourier calculation instead uses (gap, first), with gap = last - first. This file records the exact product-Haar reindexing, including the internal primitive coordinates.

No estimate and no absolute value is used here.

The endpoint shear

noncomputable def Anderson4D.r324EndpointGapFirstMeasurableEquiv : T4 × T4 ≃ᵐ T4 × T4

Reindex an ordered endpoint pair (first, last) by (last - first, first).

Equations

• Anderson4D.r324EndpointGapFirstMeasurableEquiv = (MeasurableEquiv.shearSubRight Anderson4D.T4).trans MeasurableEquiv.prodComm

@[simp]

theorem Anderson4D.r324EndpointGapFirstMeasurableEquiv_apply (first last : T4) : r324EndpointGapFirstMeasurableEquiv (first, last) = (last - first, first)

@[simp]

theorem Anderson4D.r324EndpointGapFirstMeasurableEquiv_symm_apply (gap first : T4) : r324EndpointGapFirstMeasurableEquiv.symm (gap, first) = (first, first + gap)

theorem Anderson4D.measurePreserving_r324EndpointGapFirstMeasurableEquiv : MeasureTheory.MeasurePreserving (⇑r324EndpointGapFirstMeasurableEquiv) (paperMeasure.prod paperMeasure) (paperMeasure.prod paperMeasure)

The endpoint gap-first shear preserves the paper product measure.

The full primitive head

noncomputable def Anderson4D.r324PrimitiveHeadGapFirstMeasurableEquiv (n : ℕ) (hn : 1 ≤ n) : (Fin (2 * n) → T4) ≃ᵐ (T4 × T4) × (Fin (2 * n - 2) → T4)

Split a positive-order primitive head directly into ((gap, first), internal).

Equations

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

@[simp]

theorem Anderson4D.r324PrimitiveHeadGapFirstMeasurableEquiv_symm_apply (n : ℕ) (hn : 1 ≤ n) (gap first : T4) (u : Fin (2 * n - 2) → T4) : (r324PrimitiveHeadGapFirstMeasurableEquiv n hn).symm ((gap, first), u) = primitiveAssemble n hn first (first + gap) u

theorem Anderson4D.measurePreserving_r324PrimitiveHeadGapFirstMeasurableEquiv (n : ℕ) (hn : 1 ≤ n) : MeasureTheory.MeasurePreserving (⇑(r324PrimitiveHeadGapFirstMeasurableEquiv n hn)) (MeasureTheory.Measure.pi fun (x : Fin (2 * n)) => paperMeasure) ((paperMeasure.prod paperMeasure).prod (MeasureTheory.Measure.pi fun (x : Fin (2 * n - 2)) => paperMeasure))

The complete primitive-head gap-first split preserves product Haar measure exactly.

Integral normal form

theorem Anderson4D.integral_standardBlock_eq_integral_gap_first_internal {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (n : ℕ) (hn : 1 ≤ n) (f : (Fin (2 * n) → T4) → E) (hf : MeasureTheory.Integrable f (MeasureTheory.Measure.pi fun (x : Fin (2 * n)) => paperMeasure)) : (∫ (t : Fin (2 * n) → T4), f t ∂MeasureTheory.Measure.pi fun (x : Fin (2 * n)) => paperMeasure) = ∫ (gap : T4), ∫ (first : T4), ∫ (u : Fin (2 * n - 2) → T4), f (primitiveAssemble n hn first (first + gap) u) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * n - 2)) => paperMeasure ∂paperMeasure ∂paperMeasure

Bochner integration over a genuine positive-order primitive head in the exact (gap, first, internal) order used by the incoming exceptional Fourier calculation.