Documentation

Anderson4D.Continuum.PrimitiveHigherBound

Higher-order primitive kernel bounds #

This file reconnects the real-valued R-51 scaling ledger to the ENNReal Tonelli bounds for the Bochner integrals. It closes both pointwise estimates in Proposition 4.1 for every order n ≥ 2.

theorem Anderson4D.exists_uniform_primitiveKernelBounds_ge_two {C : ℝ} (hC : PermSumEstimate C) (ρ : SmoothCutoff) :
∃ (C₂ : ℝ), 0 < C₂ ∧ ∀ (lam ε : ℝ) (n : ℕ) (hn : 2 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (supportConstant : ℝ), PrimitiveEstimateRegime n lam ε 1 supportConstant C₂ → IsAdmissiblePrimitiveInput n G → PrimitiveKernelBounds ρ lam ε n ⋯ G supportConstant C₂

The higher-order part of Proposition 4.1, uniformly in the admissible input family. The order constant is the fixed value 1, so the result covers the paper's full truncation n ≤ ⌊|log ε|⌋; the support constant is irrelevant here because the proof uses only the global term of each majorant.