Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck 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.

The real Gamma function has one minimum and diverges at both ends of its domain

Statement

As s↓0, sΓ(s)→1 and Γ(s)→+∞. As s→+∞, both Γ(s) and Γ(s)/s tend to +∞. Moreover there is a unique s0∈(1,2) at which Γ attains its global minimum; it decreases on (0,s0] and increases on [s0,∞).

Facts & Assumptions

Given: The positive smooth function Γ on (0,∞) and g:=log⁡Γ.

[F1]

For every s>0, Γ(s+1)=sΓ(s), and Γ(1)=1 (The real Gamma functional equation Γ(s+1)=sΓ(s)).

[F2]

The real Gamma function is strictly log-convex on (0,∞) (The real Gamma function is strictly log-convex).

[F3]

The real Gamma function is smooth on (0,∞) (The real Gamma function is smooth and its derivatives are logarithmic moments).

[F4]

For every natural n, Γ(n+1)=n! (Γ(n+1)=n! for every natural number n).

[F5]

For a differentiable f on an open interval, f is convex if and only if f′ is nondecreasing (A differentiable function on an open interval is convex if and only if its derivative is nondecreasing).

Proof

technique · direct
1.1F1algebra

By continuity at 1 and [F1], sΓ(s)=Γ(s+1)→Γ(1)=1 as s↓0. Since s→0+, this also gives Γ(s)→+∞.

1.2F2F6algebra

One has g(1)=g(2)=0, while strict convexity [F2] gives g(x)<0 for 1<x<2. Fixing such an x and applying [F6] on [1,x] and on [x,2] gives ξ∈(1,x) with g′(ξ)<0 and η∈(x,2) with g′(η)>0.

2.1step 1.2F2F3F5F6

By [F2] and [F5], g′ is nondecreasing. If g′(u)=g′(v) for some u<v, then g′ is constant on [u,v], so g is affine there, contradicting the strict convexity of [F2]; hence g′ is strictly increasing and has at most one zero. By [F3] it is continuous, so the sign change in step 1.2 gives exactly one zero s0∈(1,2). Strict increase makes g′ negative before s0 and positive after it, so [F6] makes g, and hence Γ, decreasing on (0,s0] and increasing on [s0,∞), and s0 is the unique global minimum.

3.1step 2.1F4algebra∎

By [F4], Γ(n+1)=n!. For n≥3, the ratios of (n−1)!/(n+1) grow by a factor exceeding 2, so this sequence tends to infinity. By the eventual increase from step 2.1, if n≤s<n+1 then Γ(s)≥Γ(n)=(n−1)! and Γ(s)/s≥(n−1)!/(n+1). Thus both quantities tend to infinity.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

71 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