LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 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.

Log-convex solutions of the Gamma recurrence obey the Bohr--Mollerup factorial squeeze

Statement

Let $f : (0, \infty) \to (0, \infty)$ be log-convex, with $f (1) = 1$ and $f (x + 1) = x f (x)$ for every $x > 0$ . For $0 < x \leq 1$ and every integer $n \geq 2$ , put

$G_{n} (x) : = \frac{n^{x} n!}{x (x + 1) \dots (x + n)} .$

Then

$G_{n} (x) \leq f (x) \leq \frac{n + x}{n} G_{n} (x) .$

Every positive log-convex $f$ with $f (1) = 1$ and $f (x + 1) = x f (x)$ lies between the Bohr--Mollerup factorial bounds, whose ratio is $(n + x) / n$ for $0 < x \leq 1$ .

Facts & Assumptions

Given: Such a function $f$ , a real $0 < x \leq 1$ , and an integer $n \geq 2$ .

[F1]

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

[F2]

Factorial is determined by $0! = 1$ and $(n + 1)! = (n + 1) n!$ (The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ ).

[F3]

For a convex $f$ on an interval, writing $s (a, b) = (f (b) - f (a)) / (b - a)$ , one has $s (x, y) \leq s (x, z) \leq s (y, z)$ whenever $x < y < z$ lie in it (For a convex function and $x < y < z$ , the three secant slopes satisfy $s (x, y) \leq s (x, z) \leq s (y, z)$ ).

Proof

technique · direct

1.1

By [F1] the function $\log f$ is convex, and the recurrence with $f (n) = (n - 1)!$ makes its secant slopes $s (n - 1, n) = \log (n - 1)$ and $s (n, n + 1) = \log n$ . For $0 < x < 1$ , [F3] at $n - 1 < n < n + x$ gives $s (n - 1, n) \leq s (n, n + x)$ and [F3] at $n < n + x < n + 1$ gives $s (n, n + x) \leq s (n, n + 1)$ ; at $x = 1$ the middle slope is $s (n, n + 1) = \log n$ itself and $\log (n - 1) \leq \log n$ . Either way $\log (n - 1) \leq (\log f (n + x) - \log f (n)) / x \leq \log n$ , and exponentiation yields $(n - 1)^{x} (n - 1)! \leq f (n + x) \leq n^{x} (n - 1)!$ .

givenF1F3cases

1.2

Iterating the recurrence gives $f (n + x) = x (x + 1) \dots (x + n - 1) f (x)$ and, by induction from [F2], $f (n) = (n - 1)!$ .

givenF2

2.1

Divide the bounds of step 1.1 by the positive product in step 1.2. Use the upper bound at $n$ and the lower bound with $n$ replaced by $n + 1$ ; both then have the common term $G_{n} (x)$ , and they become $G_{n} (x) \leq f (x) \leq ((n + x) / n) G_{n} (x)$ .

step 1.1step 1.2algebra∎

Depends on

Used by

Bohr--Mollerup characterisation of the real Gamma function Theorem

Dependency tree · two levels

34 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

K. Chandrasekharan, Lectures on the Riemann Zeta-Function, Lecture 7 §4 (standard reference, not scraped)