Complete primitive heads in the nested R-324 iteration

Paper Step 2(f) keeps the complete primitive-pairing sum grouped until the within-half removals are finished. This file supplies the corresponding one-head object for Step 3, analogous to the single-pairing single-pairing normalizedHeadDensity / properHeadIntegral interface.

No triangle inequality over primitive pairings occurs here. The complete moving-gap term is first compared with the single complete inserted kernel, and only that kernel is bounded by Proposition 4.1.

noncomputable def Anderson4D.R324NestedCrossStepContext.completeNormalizedHeadDensity {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (ρ : SmoothCutoff) (lam ε : ℝ) (t : Fin (2 * ctx.order) → T4) : ℝ

The normalized complete primitive head. The whole primitive-pairing sum is retained inside completeCrossGapPrimitiveIntegrand.

Equations

• ctx.completeNormalizedHeadDensity ρ lam ε t = Anderson4D.lamEps lam ε ^ (2 * ctx.order) * ctx.completeCrossGapPrimitiveIntegrand ρ ε ctx.normalizedInput t

theorem Anderson4D.R324NestedCrossStepContext.completeCrossGapPrimitiveIntegrand_nonneg {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (ρ : SmoothCutoff) (ε : ℝ) (G : Fin (2 * ctx.order - 1) → T4 → ℝ) (hG : ∀ (j : Fin (2 * ctx.order - 1)) (z : T4), 0 ≤ G j z) (t : Fin (2 * ctx.order) → T4) : 0 ≤ ctx.completeCrossGapPrimitiveIntegrand ρ ε G t

theorem Anderson4D.R324NestedCrossStepContext.completeNormalizedHeadDensity_nonneg {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (ρ : SmoothCutoff) (lam ε : ℝ) (t : Fin (2 * ctx.order) → T4) : 0 ≤ ctx.completeNormalizedHeadDensity ρ lam ε t

theorem Anderson4D.R324NestedCrossStepContext.completeNormalizedHeadDensity_measurable {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (ρ : SmoothCutoff) (lam ε : ℝ) : Measurable (ctx.completeNormalizedHeadDensity ρ lam ε)

theorem Anderson4D.R324NestedCrossStepContext.completeCrossGapPrimitiveIntegrand_add_const {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (ρ : SmoothCutoff) (ε : ℝ) (G : Fin (2 * ctx.order - 1) → T4 → ℝ) (t : Fin (2 * ctx.order) → T4) (a : T4) : (ctx.completeCrossGapPrimitiveIntegrand ρ ε G fun (i : Fin (2 * ctx.order)) => t i + a) = ctx.completeCrossGapPrimitiveIntegrand ρ ε G t

The complete moving-gap sum depends only on relative coordinates.

theorem Anderson4D.R324NestedCrossStepContext.completeCrossGapPrimitiveTerm_eq_diff {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossStepContext κp κm π) (ρ : SmoothCutoff) (lam ε : ℝ) (G : Fin (2 * ctx.order - 1) → T4 → ℝ) (z w : T4) : ctx.completeCrossGapPrimitiveTerm ρ lam ε G z w = ctx.completeCrossGapPrimitiveTerm ρ lam ε G (z - w) 0

Complete-sum counterpart of crossGapPrimitiveTerm_eq_diff.

noncomputable def Anderson4D.R324NestedCrossProperStepContext.completeProperHeadIntegral {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossProperStepContext κp κm π) (ρ : SmoothCutoff) (lam ε : ℝ) (left right : T4) : ℝ

The endpoint integral of a complete grouped primitive head with its two flanking inverse-square connectors.

Equations

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

theorem Anderson4D.R324NestedCrossProperStepContext.completeProperHeadIntegral_nonneg {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossProperStepContext κp κm π) (ρ : SmoothCutoff) (lam ε : ℝ) (left right : T4) : 0 ≤ ctx.completeProperHeadIntegral ρ lam ε left right

theorem Anderson4D.R324NestedCrossProperStepContext.integral_completeNormalizedHeadDensity_mul_connector {m : ℕ} {κp κm : PartialPairing (Fin m)} {π : ↥κp.singles ≃ ↥κm.singles} (ctx : R324NestedCrossProperStepContext κp κm π) (ρ : SmoothCutoff) (lam ε : ℝ) (hε : 0 < ε) (hε1 : ε ≤ 1) (post : ctx.step.PostCoordinate → T4) (hint : MeasureTheory.Integrable (fun (t : Fin (2 * ctx.step.order) → T4) => ctx.step.completeNormalizedHeadDensity ρ lam ε t * ctx.connector t post) (MeasureTheory.Measure.pi fun (x : Fin (2 * ctx.step.order)) => paperMeasure)) : (∫ (t : Fin (2 * ctx.step.order) → T4), ctx.step.completeNormalizedHeadDensity ρ lam ε t * ctx.connector t post ∂MeasureTheory.Measure.pi fun (x : Fin (2 * ctx.step.order)) => paperMeasure) = ctx.completeProperHeadIntegral ρ lam ε (post ctx.nextLeftPostCoordinate) (post ctx.nextRightPostCoordinate)

Exact Fubini identity for a complete grouped head and its two connectors.

structure Anderson4D.R324CompleteProperHeadSharpProvider (ρ : SmoothCutoff) (lam ε D : ℝ) {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : Prop

Complete-sum local analytic provider for every proper nested head.

• headIntegral_le (ctx : R324NestedCrossProperStepContext κp κm π) (left right : T4) : ctx.completeProperHeadIntegral ρ lam ε left right ≤ (D * lam) ^ (2 * ctx.step.order)

theorem Anderson4D.exists_r324CompleteProperHeadSharpProvider (ρ : SmoothCutoff) : ∃ (D : ℝ), 0 < D ∧ ∀ (lam ε : ℝ) {m : ℕ} {κp κm : PartialPairing (Fin m)} (π : ↥κp.singles ≃ ↥κm.singles), 0 < lam → 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → m ≤ truncOrder ε → R324CompleteProperHeadSharpProvider ρ lam ε D κp κm π

Proposition 4.1 and the elementary eight-dimensional convolution discharge the complete grouped proper-head provider.