Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

The continuous kernel mass

Abstract

The continuous kernel mass.

Theorem 1.1 (Extending an eventual power bound).

Lean statement: D5/S3/Arith/Robin/ForwardKernel/MellinConvergence.error_power_bound

Proof. Machine-checked in Lean as D5/S3/Arith/Robin/ForwardKernel/MellinConvergence.error_power_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let alpha>=0. If |psi(t)-t|<=Ct^alpha for every t>=t0, there is D>=0 such that |psi(t)-t|<=Dt^alpha for every t>=2. On the compact initial interval use monotonicity and nonnegativity of psi; outside it use the given estimate.

Theorem 1.2 (Power growth of the complete response).

Lean statement: D5/S3/Arith/Robin/ForwardKernel/MellinConvergence.forwardResponse_power_bound

Proof. Machine-checked in Lean as D5/S3/Arith/Robin/ForwardKernel/MellinConvergence.forwardResponse_power_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let E(t)=psi(t)-t, H(x)=x^(4/5), and T(x)=sqrt(x)/H(x)^2 times the integral from 0 to H(x) of (E(x+u)-E(x))w(x+u)/w(x). If alpha>=0, C>=0 and |E(t)|<=Ct^alpha for t>=2, then |T(x)|<=2C2^alphax^(alpha-3/10) for x>=3. The window lies in [x,2x], and its positive decreasing weight ratio is at most one.

Theorem 1.3 (Absolute convergence of the Mellin integral).

Lean statement: D5/S3/Arith/Robin/ForwardKernel/MellinConvergence.forwardMellin_integrable

Proof. Machine-checked in Lean as D5/S3/Arith/Robin/ForwardKernel/MellinConvergence.forwardMellin_integrable (✓ std3). ∎

Source. Repository-derived.

Commentary.

An eventual error bound |psi(t)-t|<=C*t^alpha with alpha>=0 implies absolute integrability of T(x)*x^(-s-1) on (x0,infinity) whenever x0>=3 and Re(s)>alpha-3/10. The response is measurable by a joint indicator representation of its variable interval integral. The majorant is a constant times x^(alpha-3/10-Re(s)-1).

Theorem 1.4 (The continuous kernel mass).

Lean statement: D5/S3/Arith/Robin/ForwardKernel/MellinConvergence.kernel_mellin_majorant_integrable

Proof. Machine-checked in Lean as D5/S3/Arith/Robin/ForwardKernel/MellinConvergence.kernel_mellin_majorant_integrable (✓ std3). ∎

Source. Repository-derived.

Commentary.

For x0>=4 and Re(s)>1/2, the function |x^(-s-1)|*moment(x,0) is integrable on [x0,infinity). The zero-exponent moment is exactly the original kernel row volume and is bounded in absolute value by (5/2)*sqrt(x). This estimate is independent of any Chebyshev error hypothesis.

References