6.2. Finite algebra🔗

Define D_h f(x) = f(x+h) + f(x−h) − 2 cos(h/2) f(x). Then

D_h cos(x/2) = 0,
D_h cosh(xt) = P_h(t) cosh(xt),
P_h(t) = 2(cosh(ht) − cos(h/2)) ≥ 0.

Iteration gives D_h^k cosh(xt) = P_h(t)^k cosh(xt). These identities are proved in FiniteDifference.lean.

Fix k ≥ 1. For 0 < h < a/(2k+1), set b_h = a−(k+1)h. Every sample in D_h^k F(b_h) lies between a−(2k+1)h and a−h. Thus all samples are inside the strip. A finite sum of absolutely integrable functions justifies moving D_h^k through the integral. It also proves integrability of the resulting weighted kernel: its absolute value is bounded by the sum of the absolute values of those finitely many integrable terms.

The cosine term vanishes. The sum of absolute coefficients of D_h^k is at most 4^k. Each sampled H value is o(h^(2k)), so

J_h = ∫₀∞ g(t) (P_h(t)/h²)^k cosh(b_h t) dt → 0.

This uses a fixed k and finitely many samples, not a uniform assertion in k.