Theorem 8.19 — Bohr–Mollerup characterization of $\Gamma$

Proved

Rudin.ch08_bohr_mollerup

by Lucas · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysisspecial-functions

If $f$ is positive on $(0,\infty)$ , $f(1) = 1$ , $f(x+1) = x f(x)$ , and $\log f$ is convex, then $f = \Gamma$ .

Preamble

import Mathlib
import Definitions.Def_Rudin_ch08_fourier

open Filter Topology

Formal statement

namespace Rudin

/-- Rudin, Theorem 8.19 (Bohr–Mollerup): a positive function `f` on `(0, ∞)` with
`f 1 = 1`, `f (x + 1) = x f x` and `log f` convex is the Gamma function. -/
theorem ch08_bohr_mollerup (f : ℝ → ℝ) (hpos : ∀ x : ℝ, 0 < x → 0 < f x)
    (hone : f 1 = 1) (hrec : ∀ x : ℝ, 0 < x → f (x + 1) = x * f x)
    (hconv : ConvexOn ℝ (Set.Ioi (0 : ℝ)) (fun x => Real.log (f x))) :
    ∀ x : ℝ, 0 < x → f x = Real.Gamma x := by sorry

end Rudin

Source

Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 8, p. 193, Theorem 8.19

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Let $f : \mathbb{R}\to\mathbb{R}$ satisfy:

$f(x) > 0$ for every $x > 0$ ;
$f(1) = 1$ ;
$f(x+1) = x\,f(x)$ for every $x > 0$ ;
$x \mapsto \log f(x)$ is convex on the open half-line $(0,\infty)$ .

Then $f(x) = \Gamma(x)$ for every real $x > 0$ .

The conclusion is restricted to positive arguments: no claim is made about $f$ at $x \le 0$ , where the hypotheses impose nothing either. The logarithm is the real logarithm (value $0$ on non-positive arguments), but on $(0,\infty)$ the positivity hypothesis makes it the genuine logarithm of $f$ .

Human review

Endorsed by Shuze Chen · Sep 13, 2026
Endorsed by Lucas · Sep 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Theorem 8.19 — Bohr–Mollerup characterization of Γ\GammaΓ

Theorem 8.19 — Bohr–Mollerup characterization of $\Gamma$