Closing one proper-block collapse

Paper: R-322 — §4.1 — closing one proper-block collapse

This file inserts the three-region inner estimate into the concrete two-variable collapse of (4.8). The first step records the Haar change of variables u = q - w; the second is the Fubini identity which exposes r322GreenDifferenceSection in the outer integral.

theorem Anderson4D.integral_r322GreenDifference_change (J : T4 → ℝ) (q : T4) : ∫ (w : T4), J (q - w) * (greenFn w - greenFn q) ∂paperMeasure = r322GreenDifferenceSection J q

Translation-reflection invariance of paper measure in exactly the orientation used by the proper-block collapse.

theorem Anderson4D.r322Collapse_eq_integral_greenDifferenceSection (Gp J : T4 → ℝ) (x : T4) (hint : MeasureTheory.Integrable (r322CollapseIntegrand Gp J greenFn x) (paperMeasure.prod paperMeasure)) : r322Collapse Gp J greenFn x = ∫ (q : T4), Gp (x - q) * r322GreenDifferenceSection J q ∂paperMeasure

Fubini and the translated Haar change of variables turn the concrete collapse into the outer convolution of the left input with the Green difference section.

theorem Anderson4D.integrable_r322Collapse_greenDifferenceSection (Gp J : T4 → ℝ) (x : T4) (hint : MeasureTheory.Integrable (r322CollapseIntegrand Gp J greenFn x) (paperMeasure.prod paperMeasure)) : MeasureTheory.Integrable (fun (q : T4) => Gp (x - q) * r322GreenDifferenceSection J q) paperMeasure

Joint integrability of the concrete collapse supplies integrability of its section form; no separate Fubini hypothesis is needed later.

Integrability of the three outer profiles

theorem Anderson4D.integrable_r322TaylorDensity_convolution {supportConstant C lam ε : ℝ} {n : ℕ} {x : T4} (hsupport : 0 < supportConstant) (hC : 0 ≤ C) (hlam : 0 ≤ lam) (hε : 0 < ε) (hε1 : ε ≤ 1) (hlog : 1 ≤ |Real.log ε|) : MeasureTheory.Integrable (fun (q : T4) => invSqKer (x - q) * r322TaylorDensity C lam ε supportConstant n q) paperMeasure

theorem Anderson4D.integrable_r322RegionTwoDensity_convolution {supportConstant C lam ε : ℝ} {n : ℕ} {x : T4} (hsupport : 0 < supportConstant) (hC : 0 ≤ C) (hlam : 0 ≤ lam) (hε : 0 < ε) (hε1 : ε ≤ 1) (hlog : 1 ≤ |Real.log ε|) (hx : x ≠ 0) : MeasureTheory.Integrable (fun (q : T4) => invSqKer (x - q) * r322RegionTwoDensity C lam ε supportConstant n q) paperMeasure

theorem Anderson4D.integrable_r322RegionThreeDensity_convolution {supportConstant C lam ε : ℝ} {n : ℕ} {x : T4} (hsupport : 0 < supportConstant) (hC : 0 ≤ C) (hlam : 0 ≤ lam) (hε : 0 < ε) (hε1 : ε ≤ 1) (hlog : 1 ≤ |Real.log ε|) : MeasureTheory.Integrable (fun (q : T4) => invSqKer (x - q) * r322RegionThreeDensity C lam ε supportConstant n q) paperMeasure

Quantitative closure of one block

theorem Anderson4D.exists_r322Collapse_le {supportConstant : ℝ} (hsupport : 0 < supportConstant) : ∃ (K : ℝ), 0 < K ∧ ∀ (C lam ε A : ℝ) (n : ℕ) (Gp J : T4 → ℝ) (x : T4), 0 ≤ C → 0 ≤ lam → 0 ≤ A → 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → x ≠ 0 → Measurable J → MemEClassT4 J → (∀ (u : T4), |J u| ≤ primitiveKernelMajorant C lam ε supportConstant n u) → (∀ (z : T4), z ≠ 0 → |Gp z| ≤ A * invSqKer z) → MeasureTheory.Integrable (r322CollapseIntegrand Gp J greenFn x) (paperMeasure.prod paperMeasure) → |r322Collapse Gp J greenFn x| ≤ A * (C * lam) ^ (2 * n) * K * invSqKer x

A proper primitive block can be collapsed without losing the inverse-square input class. The constant is chosen once before the scale, coupling, order, input kernel, primitive block, and endpoint.

theorem Anderson4D.exists_normalized_r322Collapse_admissible {supportConstant : ℝ} (hsupport : 0 < supportConstant) : ∃ (K : ℝ), 0 < K ∧ ∀ (C lam ε A : ℝ) (n : ℕ) (Gp J : T4 → ℝ), 0 < C → 0 < lam → 0 < A → 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → Measurable J → MemEClassT4 Gp → MemEClassT4 J → (∀ (u : T4), |J u| ≤ primitiveKernelMajorant C lam ε supportConstant n u) → (∀ (z : T4), z ≠ 0 → |Gp z| ≤ A * invSqKer z) → (∀ (x : T4), MeasureTheory.Integrable (r322CollapseIntegrand Gp J greenFn x) (paperMeasure.prod paperMeasure)) → ∀ (m : ℕ), IsAdmissiblePrimitiveInput m fun (x : Fin (2 * m - 1)) => normalizedOffDiagonalRepresentative (A * (C * lam) ^ (2 * n) * K) (r322Collapse Gp J greenFn)

After dividing by its proved scale factor and changing only the null diagonal, a collapsed kernel is an admissible input in every later use of Proposition 4.1. This is the analytic induction interface behind (4.13).

Abstract iteration of the analytic collapse

structure Anderson4D.R322AnalyticStage (C lam ε supportConstant : ℝ) : Type

One already-summed primitive coordinate in the interval reduction. Its fields are exactly the outputs of Proposition 4.1 used in (4.13).

• order : ℕ
• order_pos : 1 ≤ self.order
• kernel : T4 → ℝ
• measurable_kernel : Measurable self.kernel
• memE_kernel : MemEClassT4 self.kernel
• kernel_le (u : T4) : |self.kernel u| ≤ primitiveKernelMajorant C lam ε supportConstant self.order u

def Anderson4D.r322Iterate {C lam ε supportConstant : ℝ} (Gp : T4 → ℝ) : List (R322AnalyticStage C lam ε supportConstant) → T4 → ℝ

Successively insert the collapsed input produced by each primitive coordinate into the left Green slot of the next coordinate.

Equations

• Anderson4D.r322Iterate Gp [] = Gp
• Anderson4D.r322Iterate Gp (stage :: stages) = Anderson4D.r322Iterate (Anderson4D.r322Collapse Gp stage.kernel Anderson4D.greenFn) stages

def Anderson4D.R322IterationIntegrable {C lam ε supportConstant : ℝ} (Gp : T4 → ℝ) : List (R322AnalyticStage C lam ε supportConstant) → Prop

Exact Fubini licenses required by the successive concrete collapses.

Equations

• One or more equations did not get rendered due to their size.
• Anderson4D.R322IterationIntegrable Gp [] = True

theorem Anderson4D.r322Iterate_memE {C lam ε supportConstant : ℝ} {Gp : T4 → ℝ} (hGp : MemEClassT4 Gp) (stages : List (R322AnalyticStage C lam ε supportConstant)) : MemEClassT4 (r322Iterate Gp stages)

theorem Anderson4D.exists_r322Iterate_le {supportConstant : ℝ} (hsupport : 0 < supportConstant) : ∃ (K : ℝ), 0 < K ∧ ∀ (C lam ε A : ℝ) (stages : List (R322AnalyticStage C lam ε supportConstant)) (Gp : T4 → ℝ) (x : T4), 0 ≤ C → 0 ≤ lam → 0 ≤ A → 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → x ≠ 0 → (∀ (z : T4), z ≠ 0 → |Gp z| ≤ A * invSqKer z) → R322IterationIntegrable Gp stages → |r322Iterate Gp stages x| ≤ A * K ^ stages.length * (C * lam) ^ (2 * (List.map R322AnalyticStage.order stages).sum) * invSqKer x

Quantitative induction for paper (4.13). Every removed primitive coordinate contributes its exact perturbative order and one universal collapse constant; no scale or order dependence is hidden in that constant.