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

Gautschi's inequality for the real Gamma function

Statement

For x>0 and 0≤s≤1, x1−s≤Γ(x+1)/Γ(x+s)≤(x+1)1−s.

For 0<s<1 both inequalities are strict. At s=0 the lower inequality is equality, and at s=1 both are equalities.

Facts & Assumptions

Given: A real x>0 and 0≤s≤1.

[F1]

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

[F2]

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

Proof

technique · direct
1.1givenF1

Log-convexity between x and x+1 gives Γ(x+s)≤Γ(x)1−sΓ(x+1)s=xsΓ(x), strictly when 0<s<1.

1.2givenF1

Since x+1=s(x+s)+(1−s)(x+s+1), log-convexity gives Γ(x+1)≤Γ(x+s)sΓ(x+s+1)1−s=(x+s)1−sΓ(x+s)≤(x+1)1−sΓ(x+s).

2.1step 1.1step 1.2F2algebra∎

Divide the inequalities in steps 1.1 and 1.2 by positive Gamma values and use [F2]. This gives the displayed bounds and the stated strictness. Direct substitution shows the lower equality at s=0 and both equalities at s=1.

Depends on

Dependency tree · 2 levels

Sources