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

Gautschi's inequality for the real Gamma function

Statement

For $x > 0$ and $0 \leq s \leq 1$ , $x^{1 - s} \leq Γ (x + 1) / Γ (x + s) \leq (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 \leq s \leq 1$ .

[F1]

The real Gamma function is strictly log-convex on $(0, \infty)$ (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.1

Log-convexity between $x$ and $x + 1$ gives $Γ (x + s) \leq Γ (x)^{1 - s} Γ (x + 1)^{s} = x^{s} Γ (x)$ , strictly when $0 < s < 1$ .

givenF1

1.2

Since $x + 1 = s (x + s) + (1 - s) (x + s + 1)$ , log-convexity gives $Γ (x + 1) \leq Γ (x + s)^{s} Γ (x + s + 1)^{1 - s} = (x + s)^{1 - s} Γ (x + s) \leq (x + 1)^{1 - s} Γ (x + s)$ .

givenF1

2.1

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$ .

step 1.1step 1.2F2algebra∎

Depends on

Used by

Γ(1/2)=√π by Wallis's product Theorem

Dependency tree · two levels

16 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

University of Toronto MAT237Y1, The Gamma Function and the Beta Function, §1.5(c) (standard reference, not scraped)