The proper inserted convolution in R-324 Step 3

After the within-half reductions and one nested cross collapse, paper §4.2 integrates the inserted Proposition 4.1 majorant between two surviving inverse-square Green edges. This file starts the direct proof of that critical convolution. The support radius is fixed before its eventual uniform constant is selected; a constant uniform in an arbitrary support radius would be false.

noncomputable def Anderson4D.r324ProperInsertedConvolutionIntegrand (C lam ε supportConstant : ℝ) (n : ℕ) (u v : T4) (p : T4 × T4) : ℝ

Product-space form of the proper inserted convolution integrand.

Equations

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

theorem Anderson4D.r324ProperInsertedConvolutionIntegrand_eq_kernelTriple (C lam ε supportConstant : ℝ) (n : ℕ) (u v : T4) : r324ProperInsertedConvolutionIntegrand C lam ε supportConstant n u v = r324KernelTriple (primitiveInsertedMajorant C lam ε supportConstant n) u v

theorem Anderson4D.integrable_r324ProperInsertedConvolutionIntegrand (C lam supportConstant : ℝ) (n : ℕ) {ε : ℝ} (hε : 0 < ε) (u v : T4) : MeasureTheory.Integrable (r324ProperInsertedConvolutionIntegrand C lam ε supportConstant n u v) (paperMeasure.prod paperMeasure)

For every positive mollification scale, the complete proper inserted integrand is genuinely Bochner integrable on the product torus. This licenses the two applications of Fubini used in Step 3.

theorem Anderson4D.integral_r324ProperInsertedConvolutionIntegrand_eq_iterated (C lam supportConstant : ℝ) (n : ℕ) {ε : ℝ} (hε : 0 < ε) (u v : T4) : ∫ (p : T4 × T4), r324ProperInsertedConvolutionIntegrand C lam ε supportConstant n u v p ∂paperMeasure.prod paperMeasure = ∫ (a : T4), ∫ (b : T4), invSqKer (u - a) * primitiveInsertedMajorant C lam ε supportConstant n (a - b) * invSqKer (b - v) ∂paperMeasure ∂paperMeasure

Product-integral and paper iterated-integral forms agree exactly.

theorem Anderson4D.integral_r324ProperInsertedConvolutionIntegrand_eq_weightedBinary (C lam supportConstant : ℝ) (n : ℕ) {ε : ℝ} (hε : 0 < ε) (u v : T4) : ∫ (p : T4 × T4), r324ProperInsertedConvolutionIntegrand C lam ε supportConstant n u v p ∂paperMeasure.prod paperMeasure = ∫ (h : T4), primitiveInsertedMajorant C lam ε supportConstant n h * ∫ (z : T4), invSqKer (u - v - h - z) * invSqKer z ∂paperMeasure ∂paperMeasure

Exact critical-convolution form of the proper inserted integral.

theorem Anderson4D.integrable_r324ProperInsertedWeightedBinary (C lam supportConstant : ℝ) (n : ℕ) {ε : ℝ} (hε : 0 < ε) (u v : T4) : MeasureTheory.Integrable (fun (h : T4) => primitiveInsertedMajorant C lam ε supportConstant n h * ∫ (z : T4), invSqKer (u - v - h - z) * invSqKer z ∂paperMeasure) paperMeasure

The weighted-binary form is genuinely integrable; this is the certificate needed before applying the sharp binary-convolution majorant a.e.

theorem Anderson4D.integrable_primitiveInsertedMajorant_mul_criticalLogWeight {supportConstant : ℝ} (hsupport : 0 < supportConstant) (C lam : ℝ) (n : ℕ) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (hlog : 1 ≤ |Real.log ε|) (x : T4) : MeasureTheory.Integrable (fun (h : T4) => primitiveInsertedMajorant C lam ε supportConstant n h * criticalLogWeight (x - h)) paperMeasure

The inserted majorant times the moving critical logarithm is genuinely integrable.

theorem Anderson4D.exists_integral_primitiveInsertedMajorant_mul_criticalLogWeight_le {supportConstant : ℝ} (hsupport : 0 < supportConstant) : ∃ (K : ℝ), 0 < K ∧ ∀ (C lam ε : ℝ) (n : ℕ) (x : T4), 0 ≤ C → 0 ≤ lam → 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → ∫ (h : T4), primitiveInsertedMajorant C lam ε supportConstant n h * criticalLogWeight (x - h) ∂paperMeasure ≤ (C * lam) ^ (2 * n) * K

The two scale factors in the inserted Proposition 4.1 majorant cancel exactly against the local ε²|log ε| and regularized |log ε|² masses.

theorem Anderson4D.exists_r324ProperInsertedConvolution_le {supportConstant : ℝ} (hsupport : 0 < supportConstant) : ∃ (K : ℝ), 0 < K ∧ ∀ (C lam ε : ℝ) (n : ℕ) (u v : T4), 0 ≤ C → 0 ≤ lam → 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → MeasureTheory.Integrable (r324ProperInsertedConvolutionIntegrand C lam ε supportConstant n u v) (paperMeasure.prod paperMeasure) ∧ ∫ (a : T4), ∫ (b : T4), invSqKer (u - a) * primitiveInsertedMajorant C lam ε supportConstant n (a - b) * invSqKer (b - v) ∂paperMeasure ∂paperMeasure ≤ (C * lam) ^ (2 * n) * K

Sharp proper inserted convolution estimate used by every proper head of the nested R-324 reduction. The constant is selected after the fixed support radius and is uniform in the order, scale, endpoints and coupling parameters.