LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

A double-exponential envelope bounds the omitted trapezoid tails

Statement

Let $A, B, κ > 0$ , $T \geq 0$ , and let $Φ : R \to C$ be continuous with $∣ Φ (t) ∣ \leq A \exp (- B \exp (κ ∣ t ∣)) (∣ t ∣ \geq T) .$ For $h > 0$ and nonnegative integers $N_{-}, N_{+}$ with $N_{-} h, N_{+} h \geq T$ , one has $\int_{∣ t ∣ > N_{-} h on the left, N_{+} h on the right} ∣ Φ (t) ∣ d t \leq \frac{A}{κ B} (e^{- B e^{κ N_{-} h}} + e^{- B e^{κ N_{+} h}}),$ where the left and right integral means $\int_{- \infty}^{- N_{-} h} + \int_{N_{+} h}^{\infty}$ . The omitted trapezoid samples obey the same bound: $h \sum_{k < - N_{-} or k > N_{+}} ∣ Φ (k h) ∣ \leq \frac{A}{κ B} (e^{- B e^{κ N_{-} h}} + e^{- B e^{κ N_{+} h}}) .$

Facts & Assumptions

Given: $A, B, κ > 0$ , $T \geq 0$ , a continuous $Φ$ satisfying the stated envelope, $h > 0$ , and $N_{\pm} h \geq T$ .

[F1]

The real exponential function and the number $e$ by a power series and The exponential function is smooth and $(\exp)^{'} = \exp$ : $u \mapsto e^{u}$ is positive and has derivative $e^{u}$ .

[F2]

The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ : derivatives of the displayed exponential compositions are obtained by the chain rule.

[F3]

Substitution: if $φ$ is differentiable on $[c, d]$ with $φ^{'}$ integrable and $f$ is continuous on an interval containing $φ ([c, d])$ , then $\int_{φ (c)}^{φ (d)} f = \int_{c}^{d} (f \circ φ) φ^{'}$ : on finite intervals, the differentiable increasing substitution $u = B e^{κ t}$ changes the integral by its derivative factor.

[F4]

The exponential tends to $+ \infty$ at $+ \infty$ and to $0$ at $- \infty$ : $e^{- u} \to 0$ as $u \to + \infty$ .

Proof

1.1givenF1F3F4algebra

For $u_{0} = B e^{κ S}$ , finite-interval substitution from [F3] gives $\int_{S}^{R} e^{- B e^{κ t}} d t = \frac{1}{κ} \int_{u_{0}}^{B e^{κ R}} \frac{e^{- u}}{u} d u .$ For $u \geq u_{0} > 0$ , $1 / u \leq 1 / u_{0}$ , so the right side is at most $e^{- u_{0}} / (κ u_{0})$ after taking $R \to \infty$ ; the endpoint limit follows from [F4]. Since $S \geq 0$ , $e^{κ S} \geq 1$ , and each continuous one-sided tail is bounded by $e^{- B e^{κ S}} / (κ B e^{κ S}) \leq e^{- B e^{κ S}} / (κ B)$ .

2.1givenstep 1.1algebra

Apply step 1.1 with $S = N_{-} h$ to $t \mapsto ∣ Φ (- t) ∣$ and with $S = N_{+} h$ to $t \mapsto ∣ Φ (t) ∣$ , using the envelope. Adding proves the asserted integral bound and absolute integrability of both tails.

2.2givenF1F2step 1.1algebra

The function $g (t) = A e^{- B e^{κ t}}$ is nonincreasing for $t \geq 0$ , since its derivative is $- A B κ e^{κ t} e^{- B e^{κ t}} < 0$ by [F1]–[F2]. For every integer $k > N_{+}$ , $h g (k h) \leq \int_{(k - 1) h}^{k h} g (t) d t$ ; summing finite partial tails and taking their increasing limit bounds the right omitted samples by $\int_{N_{+} h}^{\infty} g (t) d t$ . The same comparison for $g (- t)$ bounds the left tail, and step 1.1 gives the stated sum bound.

3.1step 2.1step 2.2∎

The two bounds in steps 2.1 and 2.2 are finite and have the displayed right-hand side, proving both claims.

Depends on

Used by

Dependency tree · two levels

34 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

Lloyd N. Trefethen and J. A. C. Weideman, The Exponentially Convergent Trapezoidal Rule, SIAM Review 56(3), 2014 (standard reference, not scraped)