Alphabeta Math
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.

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

Statement

As s0, 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.1

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

F1algebra
1.2

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.

F2F6algebra
2.1

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.

step 1.2F2F3F5F6
3.1

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

step 2.1F4algebra

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