TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-24

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.

Euler's Gamma integral converges exactly for positive real parameters

Statement

Let $s$ be real. The Euler integral $\int_{0}^{\infty} t^{s - 1} e^{- t} d t$ converges if and only if $s > 0$ .

Facts & Assumptions

Given: A real parameter $s$ , with the integral split at $1$ .

[F1]

For every natural $m$ and real $a > 0$ , $x^{m} / \exp (a x) \to 0$ as $x \to + \infty$ (The exponential dominates every fixed nonnegative integer power at $+ \infty$ ).

[F2]

If $0 \leq u \leq v$ eventually at a singular end and the improper integral of $v$ converges there, then the integral of $u$ converges; the same assertion holds separately at infinity and at either finite singular endpoint (Comparison tests for improper integrals).

[F3]

For $x > 0$ , $\log^{'} (x) = 1 / x$ and $\log x = \int_{1}^{x} d t / t$ (The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t).

[F4]

The natural logarithm is strictly increasing and maps $(0, \infty)$ onto $R$ (Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm).

[F5]

For real $α$ , $x^{α}$ is differentiable on $(0, \infty)$ with derivative $α x^{α - 1}$ (Continuity and derivatives of positive-base real powers).

Proof

technique · direct

1.1

Suppose $s > 0$ . On $(0, 1]$ , $e^{- 1} \leq e^{- t} \leq 1$ , and [F5] with the fundamental theorem gives $\int_{0}^{1} t^{s - 1} d t = 1 / s < \infty$ . Thus [F2] gives convergence at zero.

givenF2F5algebra

1.2

If $s \leq 0$ , then $t^{s - 1} \geq t^{- 1}$ on $(0, 1]$ , while $e^{- t} \geq e^{- 1}$ . At $s = 0$ this is exactly the logarithmic threshold, and [F3] and [F4] show $\int_{0}^{1} d t / t$ diverges; the same lower comparison proves divergence for $s < 0$ .

givenF2F3F4cases

1.3

For arbitrary real $s$ , choose a natural $m \geq \max {s - 1, 0}$ . For $t \geq 1$ , $t^{s - 1} e^{- t} \leq t^{m} e^{- t}$ , and [F1] with $a = 1 / 2$ makes $t^{m} e^{- t} \leq e^{- t / 2}$ eventually. Since the latter has a convergent improper integral, [F2] gives convergence at infinity.

F1F2choose

2.1

Steps 1.1 and 1.3 prove convergence for $s > 0$ , while step 1.2 proves divergence for every $s \leq 0$ . Hence the two improper ends converge simultaneously exactly on the positive real axis.

step 1.1step 1.2step 1.3cases-exhaustive∎

Depends on

Used by

FALSE: Euler's real Gamma integral converges at the nonpositive integers False statement
The real Beta--Gamma identity Theorem
The real Gamma function is smooth and its derivatives are logarithmic moments Theorem
The real Gamma function is strictly log-convex Theorem
The real Gamma functional equation Γ(s+1)=sΓ(s) Theorem

Cited to discharge well-definedness by The real Gamma function by Euler's integral.

Dependency tree · two levels

50 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

K. Chandrasekharan, Lectures on the Riemann Zeta-Function, Lecture 6 §1(i) (standard reference, not scraped)
University of Toronto MAT237Y1, The Gamma Function and the Beta Function, §1.1 (standard reference, not scraped)