Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-30
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 locally uniformly on the right half-plane

Statement

The improper integral

0tz1etdt

converges locally uniformly on {zC:Rez>0}.

Facts & Assumptions

Given: A compact set K{z:Rez>0}.

[L1]

The real Euler integral 0ts1etdt converges exactly for s>0 (Euler's Gamma integral converges exactly for positive real parameters).

Proof

technique · direct
1.1

Since K is compact in the open right half-plane, choose real numbers 0<ab with aRezb for every zK. For 0<t1 one has tz1et=tRez1etta1, and for t1 one has tz1ettb1et.

givenchoosealgebra
2.1

By [L1], both majorants from step 1.1 have convergent improper integrals on their respective ranges. The Weierstrass M-test on compact subsets therefore gives local-uniform convergence of the truncated integrals to the Gamma integral on K.

step 1.1L1algebra

Depends on

Used by

Cited to discharge well-definedness by Euler's Gamma function on the right half-plane.

Dependency tree · two levels

11 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