LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Newman damped contour estimates

Statement

Let $f : [0, \infty) \to C$ be locally integrable with $∣ f ∣ \leq B$ , let $g (z) = \int_{0}^{\infty} f (t) e^{- z t} d t$ for $Re z > 0$ , and $g_{T} (z) = \int_{0}^{T} f (t) e^{- z t} d t$ . For $R > 0, T \geq 0$ , set $K_{R} (z) = (1 + z^{2} / R^{2}) / z$ . On the right and left semicircles $C_{+}, C_{-}$ of radius R, $∣ \int_{C_{+}} (g - g_{T}) e^{T z} K_{R} (z) d z ∣ \leq \frac{2 π B}{R}, ∣ \int_{C_{-}} g_{T} e^{T z} K_{R} (z) d z ∣ \leq \frac{2 π B}{R} .$ Integrals at the imaginary endpoints are interpreted as improper limits when needed.

Facts & Assumptions

Given: The data and hypotheses of the statement.

Proof

1.1

For $u = Re z > 0$ , $∣ g - g_{T} ∣ \leq B e^{- T u} / u$ . For $u < 0$ , $∣ g_{T} ∣ \leq B (e^{- T u} - 1) / (- u)$ , including the zero value at T=0. These inequalities follow by integrating the absolute values on the respective tail and finite interval.

givenalgebra

2.1

On $∣ z ∣ = R$ , $K_{R} (z) = 2 Re z / R^{2}$ , since $1 / z = \overline{z} / R^{2}$ . Multiplication by $∣ e^{T z} ∣$ therefore bounds either integrand by $2 B / R^{2}$ . The semicircle length is $π R$ , giving both estimates. The same uniform bound makes integrals on arcs tending to either endpoint Cauchy, so the improper endpoint interpretation exists.

step 1.1algebra∎

Depends on

Cauchy's integral formula on a circle compactly contained in a disc of holomorphy

Used by

Newman zagier tauberian theorem Theorem

Dependency tree · two levels

7 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

§1.4, proof of Theorem 1.8, right and left semicircle estimates (standard reference, not scraped)