Internal-variable majorants after the R-324 endpoint integrations

In the auxiliary endpoint-first Fubini normal form, the four external Fourier variables have already been integrated in R324EndpointBudgetClosure. This file transports its pointwise estimate through the remaining doubled internal-variable lintegral. Working first in ℝ≥0∞ is intentional: it neither assumes nor hides the finiteness which must ultimately be supplied by the successive Proposition 4.1 block collapses.

This majorant is an auxiliary endpoint-budget and integrability statement, not the signed paper-order route to the final R-324 bound: taking the pointwise norm here loses the cancellations needed for those collapses.

Measurability of the actual grouped core

theorem Anderson4D.measurable_r324RenormalizedInteriorCore {m : ℕ} (κ : PartialPairing (Fin m)) : Measurable (r324RenormalizedInteriorCore κ)

The endpoint-independent Green core is measurable in its internal variables.

theorem Anderson4D.measurable_primitiveCovarianceProduct (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (κ : PartialPairing (Fin (2 * m))) : Measurable (primitiveCovarianceProduct ρ ε m κ)

The covariance product of a fixed doubled pairing is measurable in the complete doubled internal tuple.

theorem Anderson4D.measurable_r324RefinedEndpointCore (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) (e₀ : MomentContraction m) : Measurable (r324RefinedEndpointCore ρ ε m s r e₀)

A complete residual-refined core is measurable. In particular, the finite primitive-pairing fibre is still summed before the norm.

theorem Anderson4D.measurable_r324AllRefinedEndpointCoreNormSum (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) : Measurable (r324AllRefinedEndpointCoreNormSum ρ ε m)

The complete nonnegative grouped-core budget is measurable.

Tonelli-safe endpoint budget

noncomputable def Anderson4D.r324SacrificedEndpointCoefficientLIntegral (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (α β : Z4) : ENNReal

The sacrificed endpoint-coefficient budget integrated over all doubled internal variables.

Equations

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

noncomputable def Anderson4D.r324EndpointCoreLIntegral (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) : ENNReal

The matching internal grouped-core L¹ budget.

Equations

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

theorem Anderson4D.r324SacrificedEndpointCoefficientLIntegral_le (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (hm : 0 < m) (α β : Z4) : r324SacrificedEndpointCoefficientLIntegral ρ ε m α β ≤ ENNReal.ofReal (16 * r324EndpointLoss ε α β) * r324EndpointCoreLIntegral ρ ε m

Integrated four-endpoint estimate. This is the exact Tonelli-safe bridge from the endpoint-first calculation to the remaining Proposition 4.1 majorant problem. It remains valid before finiteness of the core budget is known.

theorem Anderson4D.r324SacrificedEndpointCoefficientLIntegral_ne_top (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (hm : 0 < m) (α β : Z4) (hcore : r324EndpointCoreLIntegral ρ ε m ≠ ⊤) : r324SacrificedEndpointCoefficientLIntegral ρ ε m α β ≠ ⊤

Any finite Proposition 4.1 majorant for the grouped core immediately gives a finite endpoint budget.