Integrating the R-324 Fourier configuration series

This file proves the analytic exchange omitted in the paper's sketch of §4.2, Step 4. For a fixed full doubled pairing, the absolutely convergent covariance Fourier series may be exchanged with the genuine five-group physical integral. The proof uses joint integrability of the two renormalized Green skeletons and a summable coefficient majorant.

Green-skeleton product integrability

theorem Anderson4D.SmoothCutoff.integrable_renormalizedGreenSkeleton_flat {m : ℕ} (κ : PartialPairing (Fin m)) : MeasureTheory.Integrable (fun (p : T4 × T4 × (Fin m → T4)) => renormalizedGreenSkeleton κ (assemble p.1 p.2.1 p.2.2)) (paperMeasure.prod (paperMeasure.prod (MeasureTheory.Measure.pi fun (x : Fin m) => paperMeasure)))

Joint integrability of one renormalized Green skeleton in flat (x,y,v) coordinates.

theorem Anderson4D.SmoothCutoff.integrable_r324Flatten_renormalizedGreenSkeleton_product {m : ℕ} (κp κm : PartialPairing (Fin m)) : MeasureTheory.Integrable (r324Flatten fun (x y z w : T4) (v : Fin (2 * m) → T4) => renormalizedGreenSkeleton κp (assemble x y fun (i : Fin m) => v (leftMomentIndex i)) * renormalizedGreenSkeleton κm (assemble z w fun (i : Fin m) => v (rightMomentIndex i))) (r324PhysicalMeasure m)

The two independent Green skeletons are jointly integrable on the actual doubled physical space.

Configuration integrands

noncomputable def Anderson4D.SmoothCutoff.r324CovarianceConfigurationWeight (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (κ : PartialPairing (Fin (2 * m))) (q : Fin {i ∈ κ.pairSupport | i < κ i}.card → Z4) : ℝ

The nonnegative absolute coefficient of one Fourier assignment.

Equations

• ρ.r324CovarianceConfigurationWeight ε κ q = ∏ j : Fin {i ∈ κ.pairSupport | i < κ i}.card, ‖ρ.covarianceModeCoeff ε (q j)‖

theorem Anderson4D.SmoothCutoff.r324CovarianceConfigurationWeight_nonneg (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (κ : PartialPairing (Fin (2 * m))) (q : Fin {i ∈ κ.pairSupport | i < κ i}.card → Z4) : 0 ≤ ρ.r324CovarianceConfigurationWeight ε κ q

theorem Anderson4D.SmoothCutoff.norm_r324CovarianceFourierConfigurationTerm (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (κ : PartialPairing (Fin (2 * m))) (v : Fin (2 * m) → T4) (q : Fin {i ∈ κ.pairSupport | i < κ i}.card → Z4) : ‖ρ.r324CovarianceFourierConfigurationTerm ε κ v q‖ = ρ.r324CovarianceConfigurationWeight ε κ q

The norm of a configuration is independent of the physical coordinates: every character has norm one.

theorem Anderson4D.SmoothCutoff.summable_r324CovarianceConfigurationWeight (ρ : SmoothCutoff) {m : ℕ} {ε : ℝ} (hε : 0 < ε) (κ : PartialPairing (Fin (2 * m))) : Summable (ρ.r324CovarianceConfigurationWeight ε κ)

The configuration weights form a summable nonnegative series.

theorem Anderson4D.SmoothCutoff.measurable_r324CovarianceFourierConfigurationTerm (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (κ : PartialPairing (Fin (2 * m))) (q : Fin {i ∈ κ.pairSupport | i < κ i}.card → Z4) : Measurable fun (v : Fin (2 * m) → T4) => ρ.r324CovarianceFourierConfigurationTerm ε κ v q

A fixed Fourier configuration is measurable in the doubled internal tuple.

noncomputable def Anderson4D.SmoothCutoff.r324FullPairingFourierIntegrand (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) (q : Fin {i ∈ (↑κ).pairSupport | i < ↑κ i}.card → Z4) (x y z w : T4) (v : Fin (2 * m) → T4) : ℂ

One Fourier-configuration summand of the full-pairing physical integrand.

Equations

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

theorem Anderson4D.SmoothCutoff.momentFullPairingPhysicalIntegrand_eq_configuration_tsum (ρ : SmoothCutoff) {m : ℕ} {ε : ℝ} (hε : 0 < ε) (α β : Z4) (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) (x y z w : T4) (v : Fin (2 * m) → T4) : momentFullPairingPhysicalIntegrand ρ ε m α β κ x y z w v = ∑' (q : Fin {i ∈ (↑κ).pairSupport | i < ↑κ i}.card → Z4), ρ.r324FullPairingFourierIntegrand ε α β κ q x y z w v

The full-pairing physical integrand is pointwise the sum of its Fourier configurations.

theorem Anderson4D.SmoothCutoff.integrable_r324Flatten_fullPairingFourierIntegrand (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) (q : Fin {i ∈ (↑κ).pairSupport | i < ↑κ i}.card → Z4) : MeasureTheory.Integrable (r324Flatten (ρ.r324FullPairingFourierIntegrand ε α β κ q)) (r324PhysicalMeasure m)

Every fixed Fourier configuration is jointly integrable on the genuine physical product space.

noncomputable def Anderson4D.SmoothCutoff.r324FullPairingFourierIntegral (ρ : SmoothCutoff) {m : ℕ} (ε : ℝ) (α β : Z4) (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) (q : Fin {i ∈ (↑κ).pairSupport | i < ↑κ i}.card → Z4) : ℂ

The integrated contribution of one full-pairing Fourier configuration.

Equations

• ρ.r324FullPairingFourierIntegral ε α β κ q = ∫ (p : Anderson4D.R324PhysicalPoint m), Anderson4D.r324Flatten (ρ.r324FullPairingFourierIntegrand ε α β κ q) p ∂Anderson4D.r324PhysicalMeasure m

theorem Anderson4D.SmoothCutoff.summable_integral_norm_r324FullPairingFourierIntegrand (ρ : SmoothCutoff) {m : ℕ} {ε : ℝ} (hε : 0 < ε) (α β : Z4) (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) : Summable fun (q : Fin {i ∈ (↑κ).pairSupport | i < ↑κ i}.card → Z4) => ∫ (p : R324PhysicalPoint m), ‖r324Flatten (ρ.r324FullPairingFourierIntegrand ε α β κ q) p‖ ∂r324PhysicalMeasure m

The L¹ norms of all Fourier-configuration integrands are summable.

theorem Anderson4D.SmoothCutoff.integral_momentFullPairingPhysicalIntegrand_eq_configuration_tsum (ρ : SmoothCutoff) {m : ℕ} {ε : ℝ} (hε : 0 < ε) (α β : Z4) (κ : { τ : PartialPairing (Fin (2 * m)) // τ.IsFull }) : ∫ (p : R324PhysicalPoint m), r324Flatten (momentFullPairingPhysicalIntegrand ρ ε m α β κ) p ∂r324PhysicalMeasure m = ∑' (q : Fin {i ∈ (↑κ).pairSupport | i < ↑κ i}.card → Z4), ρ.r324FullPairingFourierIntegral ε α β κ q

The physical integral of one full pairing is exactly the countable sum of the integrals of its Fourier configurations.