Internal-cell Fubini bridge for R-324

The open-edge discretization constrains only the doubled internal variables. This file moves such a measurable constraint through the genuine five-variable product measure and puts the internal integral outside the four endpoint integrals.

This order is essential for the decaying branch of (3.24): the four endpoint Fourier integrals must be performed before a norm is taken.

def Anderson4D.r324InternalCoordinate {m : ℕ} : R324PhysicalPoint m → Fin (2 * m) → T4

The internal coordinate of the genuine R-324 physical product.

Equations

• Anderson4D.r324InternalCoordinate p = p.2.2.2.2

theorem Anderson4D.measurable_r324InternalCoordinate {m : ℕ} : Measurable r324InternalCoordinate

theorem Anderson4D.r324_setIntegral_internal_eq_internal_first {m : ℕ} (f : T4 → T4 → T4 → T4 → (Fin (2 * m) → T4) → ℂ) (S : Set (Fin (2 * m) → T4)) (hS : MeasurableSet S) (hf : MeasureTheory.Integrable (r324Flatten f) (r324PhysicalMeasure m)) : ∫ (p : R324PhysicalPoint m) in r324InternalCoordinate ⁻¹' S, r324Flatten f p ∂r324PhysicalMeasure m = ∫ (v : Fin (2 * m) → T4) in S, ∫ (x : T4), ∫ (y : T4), ∫ (z : T4), ∫ (w : T4), f x y z w v ∂paperMeasure ∂paperMeasure ∂paperMeasure ∂paperMeasure ∂MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure

A measurable restriction on only the internal variables may be moved outside all four endpoint integrations.