Common-left Fourier decay of the residual covariance product

Paper: R-324 — §4.2 Step 4(B), residual common-left Fourier decay

Paper Step 4(B) translates the whole left copy, not one covariance endpoint at a time. Under that translation the within-left and within-right residual covariances are invariant, while every cross-copy covariance sees the same one-dimensional displacement. This file records that exact grouped identity and applies the existing eighth-order periodic integration-by-parts theorem.

The coordinate estimate first differentiates only the cross factors. The grouped producer then upgrades the two invariant within-half products by the zeroth-order auxiliary estimate, so its final majorant is the complete auxiliaryCutoff residual primitive sum. No norm is taken before the complete cross product has been Fourier transformed.

The common-left coordinate line

def Anderson4D.r324CoordinateDisplacementR4 (coord : Fin dim) (t : ℝ) : R4

Euclidean displacement by t in one coordinate.

Equations

• Anderson4D.r324CoordinateDisplacementR4 coord t = Function.update 0 coord t

noncomputable def Anderson4D.r324CoordinateDisplacementT4 (coord : Fin dim) (t : ℝ) : T4

The corresponding element of the four-dimensional torus.

Equations

• Anderson4D.r324CoordinateDisplacementT4 coord t = Anderson4D.periodizeR4 (Anderson4D.r324CoordinateDisplacementR4 coord t)

theorem Anderson4D.charT4_coordinateDisplacementT4 (mode : Z4) (coord : Fin dim) (t : ℝ) : charT4 mode (r324CoordinateDisplacementT4 coord t) = (fourier (mode coord)) ↑t

The coordinate subgroup has exactly the expected one-dimensional Fourier character.

noncomputable def Anderson4D.r324CommonLeftMomentTranslation {m : ℕ} (v : Fin (2 * m) → T4) (coord : Fin dim) (t : ℝ) (j : Fin (2 * m)) : T4

Translate every vertex of the left copy by the same torus displacement, and leave every vertex of the right copy fixed.

Equations

• Anderson4D.r324CommonLeftMomentTranslation v coord t j = if ↑j < m then v j + Anderson4D.r324CoordinateDisplacementT4 coord t else v j

@[simp]

theorem Anderson4D.r324CommonLeftMomentTranslation_left {m : ℕ} (v : Fin (2 * m) → T4) (coord : Fin dim) (t : ℝ) (i : Fin m) : r324CommonLeftMomentTranslation v coord t (leftMomentIndex i) = v (leftMomentIndex i) + r324CoordinateDisplacementT4 coord t

@[simp]

theorem Anderson4D.r324CommonLeftMomentTranslation_right {m : ℕ} (v : Fin (2 * m) → T4) (coord : Fin dim) (t : ℝ) (i : Fin m) : r324CommonLeftMomentTranslation v coord t (rightMomentIndex i) = v (rightMomentIndex i)

theorem Anderson4D.add_coordinateDisplacementT4_eq_periodizeR4_update (z : T4) (coord : Fin dim) (t : ℝ) : z + r324CoordinateDisplacementT4 coord t = periodizeR4 (Function.update (torusLift z) coord (torusLift z coord + t))

A torus displacement written in the arbitrary Euclidean representative used by the covariance derivative API.

theorem Anderson4D.etaEpsT4_commonLeftTranslation_eq_coordLineFactor (rho : SmoothCutoff) (eps : ℝ) (left right : T4) (coord : Fin dim) (t : ℝ) : rho.etaEpsT4 eps (left + r324CoordinateDisplacementT4 coord t - right) = rho.etaPeriodizationCoordLineFactor eps (torusLift (left - right)) coord (torusLift (left - right) coord) t

One cross covariance under the common-left translation is exactly one factor of the common coordinate-line product.

The complete cross product

noncomputable def Anderson4D.r324MomentCrossCommonLeftCoordLineC (rho : SmoothCutoff) (eps : ℝ) {m : ℕ} (kappaPlus kappaMinus : PartialPairing (Fin m)) (pi : ↥kappaPlus.singles ≃ ↥kappaMinus.singles) (v : Fin (2 * m) → T4) (coord : Fin dim) (t : ℝ) : ℂ

The genuine residual cross-covariance product along a common-left coordinate translation.

Equations

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

theorem Anderson4D.r324MomentCrossCommonLeftCoordLineC_eq_etaProductC (rho : SmoothCutoff) (eps : ℝ) {m : ℕ} (kappaPlus kappaMinus : PartialPairing (Fin m)) (pi : ↥kappaPlus.singles ≃ ↥kappaMinus.singles) (v : Fin (2 * m) → T4) (coord : Fin dim) (t : ℝ) : r324MomentCrossCommonLeftCoordLineC rho eps kappaPlus kappaMinus pi v coord t = rho.etaPeriodizationCoordLineProductC Finset.univ eps (fun (i : ↥kappaPlus.singles) => torusLift (v (leftMomentIndex ↑i) - v (rightMomentIndex ↑(pi i)))) (fun (x : ↥kappaPlus.singles) => coord) (fun (i : ↥kappaPlus.singles) => torusLift (v (leftMomentIndex ↑i) - v (rightMomentIndex ↑(pi i))) coord) t

The common-left cross line is literally the finite coordinate-line product used by CovarianceProductFourierDecay.

theorem Anderson4D.etaAuxiliaryCoordLineProduct_eq_crossCommonLeft (rho : SmoothCutoff) (eps : ℝ) {m : ℕ} (kappaPlus kappaMinus : PartialPairing (Fin m)) (pi : ↥kappaPlus.singles ≃ ↥kappaMinus.singles) (v : Fin (2 * m) → T4) (coord : Fin dim) (t : ℝ) : rho.etaAuxiliaryCoordLineProduct Finset.univ eps (fun (i : ↥kappaPlus.singles) => torusLift (v (leftMomentIndex ↑i) - v (rightMomentIndex ↑(pi i)))) (fun (x : ↥kappaPlus.singles) => coord) (fun (i : ↥kappaPlus.singles) => torusLift (v (leftMomentIndex ↑i) - v (rightMomentIndex ↑(pi i))) coord) t = momentCrossCovarianceProduct rho.auxiliaryCutoff eps m kappaPlus kappaMinus pi (r324CommonLeftMomentTranslation v coord t)

The auxiliary coordinate-line product is the same cross product with the cutoff replaced by auxiliaryCutoff.

theorem Anderson4D.norm_fourierCoeffOn_r324MomentCrossCommonLeftCoordLineC_le (rho : SmoothCutoff) {eps : ℝ} (heps : 0 < eps) {m : ℕ} (kappaPlus kappaMinus : PartialPairing (Fin m)) (pi : ↥kappaPlus.singles ≃ ↥kappaMinus.singles) (v : Fin (2 * m) → T4) (coord : Fin dim) {n : ℤ} (hn : n ≠ 0) : ‖fourierCoeffOn ⋯ (r324MomentCrossCommonLeftCoordLineC rho eps kappaPlus kappaMinus pi v coord) n‖ ≤ |↑n|⁻¹ ^ 8 * (2 * Real.pi)⁻¹ * (↑kappaPlus.singles.card ^ 8 * rho.etaDerivativeMajorantConstant ^ kappaPlus.singles.card * eps⁻¹ ^ 8 * ∫ (t : ℝ) in -Real.pi..Real.pi, momentCrossCovarianceProduct rho.auxiliaryCutoff eps m kappaPlus kappaMinus pi (r324CommonLeftMomentTranslation v coord t))

Eighth-order Fourier decay of the entire cross family. The norm is taken only after the full cross product has been transformed.

Reassembly on one realized residual coordinate

theorem Anderson4D.pairingCovarianceProductOn_momentResidualActive_eq_threeFactor (rho : SmoothCutoff) (eps : ℝ) {m : ℕ} (kappaPlus kappaMinus : PartialPairing (Fin m)) (pi : ↥kappaPlus.singles ≃ ↥kappaMinus.singles) (v : Fin (2 * m) → T4) : pairingCovarianceProductOn rho eps (momentCombinedPairing kappaPlus kappaMinus pi) (momentResidualActive kappaPlus kappaMinus) v = ((pairingCovarianceProductOn rho eps kappaPlus (finalActive kappaPlus) fun (i : Fin m) => v (leftMomentIndex i)) * pairingCovarianceProductOn rho eps kappaMinus (finalActive kappaMinus) fun (i : Fin m) => v (rightMomentIndex i)) * momentCrossCovarianceProduct rho eps m kappaPlus kappaMinus pi v

Unmarked counterpart of the marker-preserving three-factor identity: the covariance product on the residual carrier is the product of its within-left, within-right, and cross-copy factors.

theorem Anderson4D.pairingCovarianceProductOn_left_commonLeftTranslation (rho : SmoothCutoff) (eps : ℝ) {m : ℕ} (kappa : PartialPairing (Fin m)) (v : Fin (2 * m) → T4) (coord : Fin dim) (t : ℝ) : (pairingCovarianceProductOn rho eps kappa (finalActive kappa) fun (i : Fin m) => r324CommonLeftMomentTranslation v coord t (leftMomentIndex i)) = pairingCovarianceProductOn rho eps kappa (finalActive kappa) fun (i : Fin m) => v (leftMomentIndex i)

A complete within-left residual covariance product is invariant under the common-left translation.

theorem Anderson4D.pairingCovarianceProductOn_right_commonLeftTranslation (rho : SmoothCutoff) (eps : ℝ) {m : ℕ} (kappa : PartialPairing (Fin m)) (v : Fin (2 * m) → T4) (coord : Fin dim) (t : ℝ) : (pairingCovarianceProductOn rho eps kappa (finalActive kappa) fun (i : Fin m) => r324CommonLeftMomentTranslation v coord t (rightMomentIndex i)) = pairingCovarianceProductOn rho eps kappa (finalActive kappa) fun (i : Fin m) => v (rightMomentIndex i)

A complete within-right residual covariance product is unchanged by the common-left translation.

theorem Anderson4D.etaEpsT4_le_etaDerivativeMajorantConstant_mul_auxiliary (rho : SmoothCutoff) {eps : ℝ} (heps : 0 < eps) (coord : Fin dim) (z : T4) : rho.etaEpsT4 eps z ≤ rho.etaDerivativeMajorantConstant * rho.auxiliaryCutoff.etaEpsT4 eps z

Zeroth-order member of the derivative majorant: every torus covariance is bounded by the same covariance of auxiliaryCutoff.

theorem Anderson4D.pairingCovarianceProductOn_le_auxiliary (rho : SmoothCutoff) {eps : ℝ} (heps : 0 < eps) (coord : Fin dim) {n : ℕ} (kappa : PartialPairing (Fin n)) (B : Finset (Fin n)) (v : Fin n → T4) : pairingCovarianceProductOn rho eps kappa B v ≤ rho.etaDerivativeMajorantConstant ^ {i ∈ B | i < kappa i}.card * pairingCovarianceProductOn rho.auxiliaryCutoff eps kappa B v

Product form of the preceding zeroth-order majorant.

noncomputable def Anderson4D.r324ResidualFourierMajorantBase (rho : SmoothCutoff) : ℝ

A convenient base at least one which absorbs every derivative-majorant constant produced at a fixed perturbative order.

Equations

• Anderson4D.r324ResidualFourierMajorantBase rho = max 1 rho.etaDerivativeMajorantConstant

theorem Anderson4D.one_le_r324ResidualFourierMajorantBase (rho : SmoothCutoff) : 1 ≤ r324ResidualFourierMajorantBase rho

theorem Anderson4D.etaDerivativeMajorantConstant_le_r324ResidualFourierMajorantBase (rho : SmoothCutoff) : rho.etaDerivativeMajorantConstant ≤ r324ResidualFourierMajorantBase rho

theorem Anderson4D.pairingCovarianceProductOn_le_auxiliary_orderPow (rho : SmoothCutoff) {eps : ℝ} (heps : 0 < eps) (coord : Fin dim) {m : ℕ} (kappa : PartialPairing (Fin m)) (B : Finset (Fin m)) (v : Fin m → T4) : pairingCovarianceProductOn rho eps kappa B v ≤ r324ResidualFourierMajorantBase rho ^ m * pairingCovarianceProductOn rho.auxiliaryCutoff eps kappa B v

Order-padded zeroth-order covariance-product majorant.

noncomputable def Anderson4D.r324ResidualRealizedStationaryFactorC (rho : SmoothCutoff) (eps : ℝ) {m : ℕ} (e0 : MomentContraction m) {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (he0 : e0 ∈ momentRefinedContractionFiber m s r) (coordinates : R324ResidualPrimitiveCoordinates e0.fst e0.snd.fst e0.snd.snd) (v : Fin (2 * m) → T4) : ℂ

The invariant two-half factor attached to one realized residual coordinate.

Equations

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

noncomputable def Anderson4D.r324ResidualRealizedStationaryFactor (rho : SmoothCutoff) (eps : ℝ) {m : ℕ} (e0 : MomentContraction m) {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (he0 : e0 ∈ momentRefinedContractionFiber m s r) (coordinates : R324ResidualPrimitiveCoordinates e0.fst e0.snd.fst e0.snd.snd) (v : Fin (2 * m) → T4) : ℝ

Real-valued version of the invariant two-half factor.

Equations

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

theorem Anderson4D.r324ResidualRealizedStationaryFactorC_eq_coe (rho : SmoothCutoff) (eps : ℝ) {m : ℕ} (e0 : MomentContraction m) {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (he0 : e0 ∈ momentRefinedContractionFiber m s r) (coordinates : R324ResidualPrimitiveCoordinates e0.fst e0.snd.fst e0.snd.snd) (v : Fin (2 * m) → T4) : r324ResidualRealizedStationaryFactorC rho eps e0 he0 coordinates v = ↑(r324ResidualRealizedStationaryFactor rho eps e0 he0 coordinates v)

theorem Anderson4D.r324ResidualRealizedStationaryFactor_nonneg (rho : SmoothCutoff) (eps : ℝ) {m : ℕ} (e0 : MomentContraction m) {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (he0 : e0 ∈ momentRefinedContractionFiber m s r) (coordinates : R324ResidualPrimitiveCoordinates e0.fst e0.snd.fst e0.snd.snd) (v : Fin (2 * m) → T4) : 0 ≤ r324ResidualRealizedStationaryFactor rho eps e0 he0 coordinates v

theorem Anderson4D.norm_r324ResidualRealizedStationaryFactorC (rho : SmoothCutoff) (eps : ℝ) {m : ℕ} (e0 : MomentContraction m) {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (he0 : e0 ∈ momentRefinedContractionFiber m s r) (coordinates : R324ResidualPrimitiveCoordinates e0.fst e0.snd.fst e0.snd.snd) (v : Fin (2 * m) → T4) : ‖r324ResidualRealizedStationaryFactorC rho eps e0 he0 coordinates v‖ = r324ResidualRealizedStationaryFactor rho eps e0 he0 coordinates v

theorem Anderson4D.r324ResidualRealizedStationaryFactor_le_auxiliary (rho : SmoothCutoff) {eps : ℝ} (heps : 0 < eps) (coord : Fin dim) {m : ℕ} (e0 : MomentContraction m) {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (he0 : e0 ∈ momentRefinedContractionFiber m s r) (coordinates : R324ResidualPrimitiveCoordinates e0.fst e0.snd.fst e0.snd.snd) (v : Fin (2 * m) → T4) : r324ResidualRealizedStationaryFactor rho eps e0 he0 coordinates v ≤ r324ResidualFourierMajorantBase rho ^ (2 * m) * r324ResidualRealizedStationaryFactor rho.auxiliaryCutoff eps e0 he0 coordinates v

Both stationary half-products may be upgraded to the auxiliary cutoff at an exponential-in-order cost.

One realized residual coordinate

noncomputable def Anderson4D.r324ResidualPrimitiveCoordinateCommonLeftCoordLineC (rho : SmoothCutoff) (eps : ℝ) {m : ℕ} (e0 : MomentContraction m) (coordinates : R324ResidualPrimitiveCoordinates e0.fst e0.snd.fst e0.snd.snd) (v : Fin (2 * m) → T4) (coord : Fin dim) (t : ℝ) : ℂ

One realized residual-coordinate product along the common-left line.

Equations

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

theorem Anderson4D.r324ResidualPrimitiveCoordinateCommonLeftCoordLineC_eq (rho : SmoothCutoff) (eps : ℝ) {m : ℕ} (e0 : MomentContraction m) {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (he0 : e0 ∈ momentRefinedContractionFiber m s r) (coordinates : R324ResidualPrimitiveCoordinates e0.fst e0.snd.fst e0.snd.snd) (v : Fin (2 * m) → T4) (coord : Fin dim) (t : ℝ) : r324ResidualPrimitiveCoordinateCommonLeftCoordLineC rho eps e0 coordinates v coord t = r324ResidualRealizedStationaryFactorC rho eps e0 he0 coordinates v * r324MomentCrossCommonLeftCoordLineC rho eps (↑(r324RefinedContractionOfResidualCoordinates e0 he0 coordinates)).fst (↑(r324RefinedContractionOfResidualCoordinates e0 he0 coordinates)).snd.fst (↑(r324RefinedContractionOfResidualCoordinates e0 he0 coordinates)).snd.snd v coord t

Exact factorization of a realized residual-coordinate line into the stationary within-half factor and the complete common-left cross line.

theorem Anderson4D.momentCrossCovarianceProduct_nonneg_local (rho : SmoothCutoff) (eps : ℝ) {m : ℕ} (kappaPlus kappaMinus : PartialPairing (Fin m)) (pi : ↥kappaPlus.singles ≃ ↥kappaMinus.singles) (v : Fin (2 * m) → T4) : 0 ≤ momentCrossCovarianceProduct rho eps m kappaPlus kappaMinus pi v

Nonnegativity of the complete residual cross product.

theorem Anderson4D.norm_fourierCoeffOn_r324MomentCrossCommonLeftCoordLineC_le_orderPow (rho : SmoothCutoff) {eps : ℝ} (heps : 0 < eps) {m : ℕ} (kappaPlus kappaMinus : PartialPairing (Fin m)) (pi : ↥kappaPlus.singles ≃ ↥kappaMinus.singles) (v : Fin (2 * m) → T4) (coord : Fin dim) {n : ℤ} (hn : n ≠ 0) : ‖fourierCoeffOn ⋯ (r324MomentCrossCommonLeftCoordLineC rho eps kappaPlus kappaMinus pi v coord) n‖ ≤ |↑n|⁻¹ ^ 8 * (2 * Real.pi)⁻¹ * (↑m ^ 8 * r324ResidualFourierMajorantBase rho ^ m * eps⁻¹ ^ 8 * ∫ (t : ℝ) in -Real.pi..Real.pi, momentCrossCovarianceProduct rho.auxiliaryCutoff eps m kappaPlus kappaMinus pi (r324CommonLeftMomentTranslation v coord t))

Order-uniform version of the grouped cross Fourier estimate.

theorem Anderson4D.integral_r324ResidualPrimitiveCoordinateCommonLeft_auxiliary_eq (rho : SmoothCutoff) (eps : ℝ) {m : ℕ} (e0 : MomentContraction m) {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (he0 : e0 ∈ momentRefinedContractionFiber m s r) (coordinates : R324ResidualPrimitiveCoordinates e0.fst e0.snd.fst e0.snd.snd) (v : Fin (2 * m) → T4) (coord : Fin dim) : ∫ (t : ℝ) in -Real.pi..Real.pi, r324ResidualPrimitiveCoordinateProduct rho.auxiliaryCutoff eps e0.fst e0.snd.fst e0.snd.snd coordinates (r324CommonLeftMomentTranslation v coord t) = r324ResidualRealizedStationaryFactor rho.auxiliaryCutoff eps e0 he0 coordinates v * ∫ (t : ℝ) in -Real.pi..Real.pi, momentCrossCovarianceProduct rho.auxiliaryCutoff eps m (↑(r324RefinedContractionOfResidualCoordinates e0 he0 coordinates)).fst (↑(r324RefinedContractionOfResidualCoordinates e0 he0 coordinates)).snd.fst (↑(r324RefinedContractionOfResidualCoordinates e0 he0 coordinates)).snd.snd (r324CommonLeftMomentTranslation v coord t)

Recombination identity for the auxiliary coordinate product.

theorem Anderson4D.norm_fourierCoeffOn_r324ResidualPrimitiveCoordinateCommonLeftCoordLineC_le_auxiliary (rho : SmoothCutoff) {eps : ℝ} (heps : 0 < eps) {m : ℕ} (e0 : MomentContraction m) {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (he0 : e0 ∈ momentRefinedContractionFiber m s r) (coordinates : R324ResidualPrimitiveCoordinates e0.fst e0.snd.fst e0.snd.snd) (v : Fin (2 * m) → T4) (coord : Fin dim) {n : ℤ} (hn : n ≠ 0) : ‖fourierCoeffOn ⋯ (r324ResidualPrimitiveCoordinateCommonLeftCoordLineC rho eps e0 coordinates v coord) n‖ ≤ |↑n|⁻¹ ^ 8 * (2 * Real.pi)⁻¹ * (↑m ^ 8 * r324ResidualFourierMajorantBase rho ^ (3 * m) * eps⁻¹ ^ 8 * ∫ (t : ℝ) in -Real.pi..Real.pi, r324ResidualPrimitiveCoordinateProduct rho.auxiliaryCutoff eps e0.fst e0.snd.fst e0.snd.snd coordinates (r324CommonLeftMomentTranslation v coord t))

Fully auxiliary-cutoff, order-uniform decay for one realized residual coordinate. This is the form which recombines after summing coordinates.

theorem Anderson4D.norm_fourierCoeffOn_r324ResidualPrimitiveCoordinateCommonLeftCoordLineC_le (rho : SmoothCutoff) {eps : ℝ} (heps : 0 < eps) {m : ℕ} (e0 : MomentContraction m) {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (he0 : e0 ∈ momentRefinedContractionFiber m s r) (coordinates : R324ResidualPrimitiveCoordinates e0.fst e0.snd.fst e0.snd.snd) (v : Fin (2 * m) → T4) (coord : Fin dim) {n : ℤ} (hn : n ≠ 0) : ‖fourierCoeffOn ⋯ (r324ResidualPrimitiveCoordinateCommonLeftCoordLineC rho eps e0 coordinates v coord) n‖ ≤ ‖r324ResidualRealizedStationaryFactorC rho eps e0 he0 coordinates v‖ * (|↑n|⁻¹ ^ 8 * (2 * Real.pi)⁻¹ * (↑(↑(r324RefinedContractionOfResidualCoordinates e0 he0 coordinates)).fst.singles.card ^ 8 * rho.etaDerivativeMajorantConstant ^ (↑(r324RefinedContractionOfResidualCoordinates e0 he0 coordinates)).fst.singles.card * eps⁻¹ ^ 8 * ∫ (t : ℝ) in -Real.pi..Real.pi, momentCrossCovarianceProduct rho.auxiliaryCutoff eps m (↑(r324RefinedContractionOfResidualCoordinates e0 he0 coordinates)).fst (↑(r324RefinedContractionOfResidualCoordinates e0 he0 coordinates)).snd.fst (↑(r324RefinedContractionOfResidualCoordinates e0 he0 coordinates)).snd.snd (r324CommonLeftMomentTranslation v coord t)))

Eighth-order common-left Fourier decay for one realized residual coordinate. The analytic output is the mixed-cutoff product dictated by the derivative allocation: the invariant factors keep rho, while every cross factor uses rho.auxiliaryCutoff.

The grouped residual primitive sum

noncomputable def Anderson4D.r324ResidualPrimitiveSumCommonLeftCoordLineC (rho : SmoothCutoff) (eps : ℝ) {m : ℕ} (e0 : MomentContraction m) (v : Fin (2 * m) → T4) (coord : Fin dim) (t : ℝ) : ℂ

The complete residual primitive sum along the common-left coordinate line. The finite primitive-coordinate family remains grouped inside this function.

Equations

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

theorem Anderson4D.r324ResidualPrimitiveSumCommonLeftCoordLineC_eq_sum (rho : SmoothCutoff) (eps : ℝ) {m : ℕ} (e0 : MomentContraction m) (v : Fin (2 * m) → T4) (coord : Fin dim) (t : ℝ) : r324ResidualPrimitiveSumCommonLeftCoordLineC rho eps e0 v coord t = ∑ coordinates : R324ResidualPrimitiveCoordinates e0.fst e0.snd.fst e0.snd.snd, r324ResidualPrimitiveCoordinateCommonLeftCoordLineC rho eps e0 coordinates v coord t

Exact finite-coordinate expansion of the grouped common-left line.

theorem Anderson4D.intervalIntegrable_r324ResidualPrimitiveCoordinateCommonLeftCoordLineC (rho : SmoothCutoff) {eps : ℝ} (heps : 0 < eps) {m : ℕ} (e0 : MomentContraction m) {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (he0 : e0 ∈ momentRefinedContractionFiber m s r) (coordinates : R324ResidualPrimitiveCoordinates e0.fst e0.snd.fst e0.snd.snd) (v : Fin (2 * m) → T4) (coord : Fin dim) : IntervalIntegrable (r324ResidualPrimitiveCoordinateCommonLeftCoordLineC rho eps e0 coordinates v coord) MeasureTheory.volume (-Real.pi) Real.pi

Every realized coordinate line is interval-integrable.

theorem Anderson4D.fourierCoeffOn_r324ResidualPrimitiveSumCommonLeftCoordLineC_eq_sum (rho : SmoothCutoff) {eps : ℝ} (heps : 0 < eps) {m : ℕ} (e0 : MomentContraction m) {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (he0 : e0 ∈ momentRefinedContractionFiber m s r) (v : Fin (2 * m) → T4) (coord : Fin dim) (n : ℤ) : fourierCoeffOn ⋯ (r324ResidualPrimitiveSumCommonLeftCoordLineC rho eps e0 v coord) n = ∑ coordinates : R324ResidualPrimitiveCoordinates e0.fst e0.snd.fst e0.snd.snd, fourierCoeffOn ⋯ (r324ResidualPrimitiveCoordinateCommonLeftCoordLineC rho eps e0 coordinates v coord) n

Fourier coefficient commutes with the finite residual-coordinate sum. This is the only triangle-inequality seam in the grouped theorem.

theorem Anderson4D.norm_fourierCoeffOn_r324ResidualPrimitiveSumCommonLeftCoordLineC_le (rho : SmoothCutoff) {eps : ℝ} (heps : 0 < eps) {m : ℕ} (e0 : MomentContraction m) {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (he0 : e0 ∈ momentRefinedContractionFiber m s r) (v : Fin (2 * m) → T4) (coord : Fin dim) {n : ℤ} (hn : n ≠ 0) : ‖fourierCoeffOn ⋯ (r324ResidualPrimitiveSumCommonLeftCoordLineC rho eps e0 v coord) n‖ ≤ ∑ coordinates : R324ResidualPrimitiveCoordinates e0.fst e0.snd.fst e0.snd.snd, ‖r324ResidualRealizedStationaryFactorC rho eps e0 he0 coordinates v‖ * (|↑n|⁻¹ ^ 8 * (2 * Real.pi)⁻¹ * (↑(↑(r324RefinedContractionOfResidualCoordinates e0 he0 coordinates)).fst.singles.card ^ 8 * rho.etaDerivativeMajorantConstant ^ (↑(r324RefinedContractionOfResidualCoordinates e0 he0 coordinates)).fst.singles.card * eps⁻¹ ^ 8 * ∫ (t : ℝ) in -Real.pi..Real.pi, momentCrossCovarianceProduct rho.auxiliaryCutoff eps m (↑(r324RefinedContractionOfResidualCoordinates e0 he0 coordinates)).fst (↑(r324RefinedContractionOfResidualCoordinates e0 he0 coordinates)).snd.fst (↑(r324RefinedContractionOfResidualCoordinates e0 he0 coordinates)).snd.snd (r324CommonLeftMomentTranslation v coord t)))

Grouped common-left Fourier estimate for the residual primitive sum. It is honest but still mixed-cutoff: each summand keeps its invariant within-half covariance factors at rho, while the transformed cross family uses rho.auxiliaryCutoff.

theorem Anderson4D.intervalIntegrable_r324ResidualPrimitiveCoordinateCommonLeft_auxiliary (rho : SmoothCutoff) {eps : ℝ} (heps : 0 < eps) {m : ℕ} (e0 : MomentContraction m) {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (he0 : e0 ∈ momentRefinedContractionFiber m s r) (coordinates : R324ResidualPrimitiveCoordinates e0.fst e0.snd.fst e0.snd.snd) (v : Fin (2 * m) → T4) (coord : Fin dim) : IntervalIntegrable (fun (t : ℝ) => r324ResidualPrimitiveCoordinateProduct rho.auxiliaryCutoff eps e0.fst e0.snd.fst e0.snd.snd coordinates (r324CommonLeftMomentTranslation v coord t)) MeasureTheory.volume (-Real.pi) Real.pi

Real auxiliary coordinate lines are interval-integrable.

theorem Anderson4D.norm_fourierCoeffOn_r324ResidualPrimitiveSumCommonLeftCoordLineC_le_auxiliary (rho : SmoothCutoff) {eps : ℝ} (heps : 0 < eps) {m : ℕ} (e0 : MomentContraction m) {s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))} (he0 : e0 ∈ momentRefinedContractionFiber m s r) (v : Fin (2 * m) → T4) (coord : Fin dim) {n : ℤ} (hn : n ≠ 0) : ‖fourierCoeffOn ⋯ (r324ResidualPrimitiveSumCommonLeftCoordLineC rho eps e0 v coord) n‖ ≤ |↑n|⁻¹ ^ 8 * (2 * Real.pi)⁻¹ * (↑m ^ 8 * r324ResidualFourierMajorantBase rho ^ (3 * m) * eps⁻¹ ^ 8) * ∫ (t : ℝ) in -Real.pi..Real.pi, r324ResidualPrimitiveSumProduct rho.auxiliaryCutoff eps e0.fst e0.snd.fst e0.snd.snd (r324CommonLeftMomentTranslation v coord t)

Grouped common-left residual Fourier producer. After upgrading the two stationary families by the zeroth-order auxiliary estimate, the finite coordinate sum recombines exactly into the complete residual primitive sum of auxiliaryCutoff. The loss remains exponential in the perturbative order and is therefore absorbable into the paper's named base constant.