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 is strictly log-convex

Statement

The real Gamma function is strictly log-convex on $(0, \infty)$ .

Facts & Assumptions

Given: Distinct $x, y > 0$ and a weight $0 < λ < 1$ .

[F1]

For $0 < λ < 1$ , exponential convexity is strict unless its two arguments are equal (The two-point convexity inequality for the exponential function).

[F2]

A positive function is log-convex when its logarithm is convex (Log-convex positive functions).

Proof

technique · direct

1.1givenF1

Fix $c > 0$ and write $c^{s} Γ (s) = \int_{0}^{\infty} t^{- 1} e^{- t} \exp (s \log (c t)) d t$ . By [F1], the integrand at $(1 - λ) x + λ y$ is at most the corresponding convex combination, with strict inequality except at the single point $t = 1 / c$ ; integration makes $s \mapsto c^{s} Γ (s)$ strictly convex.

1.2constructalgebra

Choose $c = (Γ (x) / Γ (y))^{1 / (y - x)} > 0$ . Then $c^{x} Γ (x) = c^{y} Γ (y)$ .

2.1step 1.1step 1.2F2algebra∎

Apply step 1.1 at $x, y$ with the $c$ from step 1.2. After cancelling $c^{(1 - λ) x + λ y}$ , one gets $Γ ((1 - λ) x + λ y) < Γ (x)^{1 - λ} Γ (y)^{λ}$ , which is strict log-convexity by [F2].

The real Gamma function is strictly log-convex

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources