Analytic bounds at the first primitive order

The exact n = 1 formulas from PrimitiveBase are closed here using the periodized covariance estimates. This isolates the base case of paper §5 from the Hepp-tree argument needed at higher orders.

theorem Anderson4D.lamEps_sq {lam ε : ℝ} (hlog : 0 < |Real.log ε|) : lamEps lam ε ^ 2 = lam ^ 2 / |Real.log ε|

Squaring the logarithmically scaled coupling removes the square root.

theorem Anderson4D.abs_lamEps_even_pow {lam ε : ℝ} (n : ℕ) (hlog : 0 < |Real.log ε|) : |lamEps lam ε| ^ (2 * n) = lam ^ (2 * n) / |Real.log ε| ^ n

Exact all-order coupling ledger used throughout Propositions 4.1 and 3.5: every pair of noise factors contributes one power of |log ε|⁻¹.

theorem Anderson4D.primitiveKernelDiff_one_le_local (ρ : SmoothCutoff) {lam ε Cη C supportConstant : ℝ} (hε : 0 < ε) (hlog : 0 < |Real.log ε|) (heta : ∀ (z : T4), ρ.etaEpsT4 ε z ≤ ε⁻¹ ^ dim * Cη) (hC : Cη ≤ C ^ 2) (hsupport : 4 * ρ.radius ≤ supportConstant) (G : Fin 1 → T4 → ℝ) (hG : ∀ (z : T4), |G 0 z| ≤ invSqKer z) (z : T4) : |primitiveKernelDiff ρ lam ε 1 ⋯ G z| ≤ (C * lam) ^ 2 * (ε⁻¹ ^ 4 / |Real.log ε| * invSqKer z * primitiveSupportIndicator supportConstant ε z)

The ordinary n = 1 kernel is controlled by the local term in (4.3). The covariance constant and the support radius remain explicit.

theorem Anderson4D.primitiveKernelInsertedDiff_one_le_local (ρ : SmoothCutoff) {lam ε Cη C supportConstant : ℝ} (hε : 0 < ε) (hlog : 0 < |Real.log ε|) (heta : ∀ (z : T4), ρ.etaEpsT4 ε z ≤ ε⁻¹ ^ dim * Cη) (hC : Cη * (1 + supportConstant ^ 2) ≤ C ^ 2) (hsupport : 4 * ρ.radius ≤ supportConstant) (G : Fin 1 → T4 → ℝ) (hG : ∀ (z : T4), |G 0 z| ≤ invSqKer z) (z : T4) : |primitiveKernelInsertedDiff ρ lam ε 1 ⋯ G z| ≤ (C * lam) ^ 2 * (ε⁻¹ ^ 2 / |Real.log ε| * invSqKer z * primitiveSupportIndicator supportConstant ε z)

The inserted n = 1 kernel is controlled by the local term in (4.4). The additional factor is paid for by the explicit covariance support.

theorem Anderson4D.primitiveKernelBounds_one (ρ : SmoothCutoff) {lam ε Cη C supportConstant : ℝ} (hε : 0 < ε) (_hε1 : ε ≤ 1) (hlog : 0 < |Real.log ε|) (hlam : 0 ≤ lam) (hCnonneg : 0 ≤ C) (heta : ∀ (z : T4), ρ.etaEpsT4 ε z ≤ ε⁻¹ ^ dim * Cη) (hCordinary : Cη ≤ C ^ 2) (hCinserted : Cη * (1 + supportConstant ^ 2) ≤ C ^ 2) (hsupport : 4 * ρ.radius ≤ supportConstant) (G : Fin 1 → T4 → ℝ) (hG : ∀ (z : T4), |G 0 z| ≤ invSqKer z) : PrimitiveKernelBounds ρ lam ε 1 ⋯ G supportConstant C

The two base-order local terms imply the full (4.3)--(4.4) majorants, since their long-range terms are nonnegative.