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.