The Bohr–Mollerup theorem

The gamma function is defined for $x>0$ by Euler’s integral

\Gamma(x)=\int_0^\infty t^{x-1}e^{-t}\,\mathrm{d}t .

(1)

It extends the factorial, $\Gamma(n)=(n-1)!$ , and satisfies $\Gamma(x+1)=x\,\Gamma(x)$ . But infinitely many functions interpolate the factorial. The Bohr–Mollerup theorem Bohr & Mollerup, 1922, given the elegant treatment reproduced here by Artin Artin, 1964, singles out $\Gamma$ by one extra qualitative condition: logarithmic convexity.

Theorem (Bohr–Mollerup). The gamma function is the unique function $f\colon(0,\infty)\to(0,\infty)$ that simultaneously satisfies

$f(1)=1$ ;
$f(x+1)=x\,f(x)$ for all $x>0$ ;
$\log f$ is convex on $(0,\infty)$ .

Here “log-convex” means that $\log\circ f$ is a convex function; equivalently $f\big(\lambda a+(1-\lambda)b\big)\le f(a)^{\lambda}f(b)^{1-\lambda}$ for $\lambda\in[0,1]$ .

Lean formalization

The statements and proofs in this note are formalized in Lean 4 + Mathlib in BohrMollerupFlow.lean, a flow-faithful development that reproduces the note’s steps in order. The three hypotheses are bundled in a predicate GammaLike; the elementary recurrence identities (Steps 1) are proved from scratch by induction, while the analytic squeeze of Steps 2–3 — monotonicity of the secant slopes of $\log f$ and the fact that $\log(n+1)-\log n\to 0$ — is supplied by Mathlib’s Real.BohrMollerup development and assembled here into the note’s flow. Each Lean proof dropdown below splices the corresponding declaration verbatim from the compiled source, so the displayed code cannot drift from what is actually checked. Continuous integration runs lake build (which fails on any error or sorry), and the file is axiom-clean (propext, Classical.choice, Quot.sound).

Lean’s kernel guarantees each proof is correct. Whether a Lean statement faithfully captures the informal claim is a human judgement, so each dropdown is placed next to the statement it formalizes, for direct comparison.

BohrMollerupFlow.lean

/-- The three Bohr–Mollerup hypotheses on a function `f : ℝ → ℝ`, packaged as a predicate:
`f` is positive and log-convex on `(0, ∞)`, satisfies `f (x + 1) = x · f x`, and `f 1 = 1`.
The theorem below says `Real.Gamma` is the unique such function. -/
structure GammaLike (f : ℝ → ℝ) : Prop where
  /-- `f` is positive on the positive reals. -/
  pos : ∀ x, 0 < x → 0 < f x
  /-- The Gamma functional equation `f (x + 1) = x · f x`. -/
  functional_eq : ∀ x, 0 < x → f (x + 1) = x * f x
  /-- `log ∘ f` is convex on the positive reals (i.e. `f` is log-convex). -/
  log_convex : ConvexOn ℝ (Ioi 0) (Real.log ∘ f)
  /-- Normalization `f 1 = 1`. -/
  one : f 1 = 1

BohrMollerupFlow.lean

/-- **The Bohr–Mollerup theorem.** `Real.Gamma` is `GammaLike`, and it is the *unique* `GammaLike`
function: every function that is positive and log-convex on `(0, ∞)`, satisfies
`f (x + 1) = x · f x`, and has `f 1 = 1`, coincides with `Real.Gamma` on `(0, ∞)`. -/
theorem bohr_mollerup :
    GammaLike Real.Gamma ∧ ∀ f, GammaLike f → EqOn f Real.Gamma (Ioi 0) :=
  ⟨gammaLike_Gamma, fun _ hf => hf.eq_Gamma⟩

The proof has two halves: uniqueness (any $f$ with properties 1–3 is forced to equal a specific limit, hence equals $\Gamma$ ) and existence ( $\Gamma$ itself has all three properties). The heart of the argument is uniqueness.

Step 1: the functional equation reproduces the factorials¶

Assume $f$ satisfies properties 1–3. Property 2 applied repeatedly, with $f(1)=1$ , gives by induction

f(n+1)=n! \qquad (n\in\mathbb{N}),

(2)

so $f$ interpolates the factorials just like $\Gamma$ . More generally, iterating $f(x+1)=x\,f(x)$ exactly $n$ times yields the product formula

f(x+n)=f(x)\,\prod_{m=0}^{n-1}(x+m)=x(x+1)\cdots(x+n-1)\,f(x).

(3)

The consequence is decisive: (3) lets us recover $f(x)$ for any $x>0$ from its values on the unit interval $(0,1]$ . So it suffices to pin down $f$ on $(0,1]$ .

BohrMollerupFlow.lean

/-- **The functional equation forces the factorials.** From `f (x + 1) = x · f x` and `f 1 = 1`,
induction gives `f (n + 1) = n !` for every natural number `n`; in particular `f` interpolates the
factorials, `f n = (n − 1)!`. -/
theorem GammaLike.f_nat (hf : GammaLike f) (n : ℕ) : f (n + 1) = n ! := by
  induction n with
  | zero => simpa using hf.one
  | succ k ih =>
    have hk : (0 : ℝ) < (k : ℝ) + 1 := by positivity
    have hrec := hf.functional_eq ((k : ℝ) + 1) hk
    rw [Nat.cast_succ, hrec, ih, Nat.factorial_succ]
    push_cast
    ring

BohrMollerupFlow.lean

/-- **The functional equation as a product.** Iterating `f (x + 1) = x · f x` `n` times gives
`f (x + n) = f x · x (x + 1) ⋯ (x + n − 1)`, i.e. `f (x + n) = f x · ∏_{m < n} (x + m)`. Knowing `f`
on `(0, 1]` therefore determines it everywhere on `(0, ∞)`. -/
theorem GammaLike.f_add_nat (hf : GammaLike f) (hx : 0 < x) (n : ℕ) :
    f (x + n) = f x * ∏ m ∈ Finset.range n, (x + m) := by
  induction n with
  | zero => simp
  | succ k ih =>
    have hxk : 0 < x + (k : ℝ) := by positivity
    have hrec := hf.functional_eq (x + (k : ℝ)) hxk
    have hcast : x + ((k : ℕ) + 1 : ℕ) = (x + (k : ℝ)) + 1 := by push_cast; ring
    rw [hcast, hrec, ih, Finset.prod_range_succ]
    ring

Step 2: log-convexity sandwiches the values¶

Fix $x$ with $0<x\le 1$ and write $\varphi:=\log f$ , which is convex by property 3. For $x_1<x_2$ let

S(x_1,x_2)=\frac{\varphi(x_2)-\varphi(x_1)}{x_2-x_1}

(4)

be the slope of the secant of $\varphi$ over $[x_1,x_2]$ . Convexity is exactly the statement that $S$ is monotonically increasing in each argument. For an integer $n\ge 2$ consider the four points $n-1<n<n+x\le n+1$ . Monotonicity of the slopes gives

S(n-1,\,n)\;\le\;S(n,\,n+x)\;\le\;S(n,\,n+1).

(5)

By (2), $\varphi(n)=\log\big((n-1)!\big)$ and $\varphi(n+1)=\log(n!)$ , so the outer slopes collapse to logarithms of integers, $S(n-1,n)=\log(n-1)$ and $S(n,n+1)=\log n$ , while the middle slope is $S(n,n+x)=\big(\varphi(n+x)-\varphi(n)\big)/x$ . Multiplying (5) by $x>0$ and adding $\varphi(n)$ turns it into a sandwich of $\varphi(n+x)$ between two lines in $x$ :

\log\big(f(n)\big)+x\log(n-1)\;\le\;\log\big(f(n+x)\big)\;\le\;\log\big(f(n)\big)+x\log n .

(6)

BohrMollerupFlow.lean

/-- **The log-convexity sandwich.** For `0 < x ≤ 1` and `n ≥ 2`, convexity of `log ∘ f` forces the
secant slopes of `log ∘ f` to be monotone, which traps `log (f (n + x))` between the two lines in
`x` through the lattice values of `log ∘ f`:
`log (f n) + x·log (n − 1) ≤ log (f (n + x)) ≤ log (f n) + x·log n`. -/
theorem GammaLike.log_sandwich (hf : GammaLike f) (hn : 2 ≤ n) (hx : 0 < x) (hx' : x ≤ 1) :
    Real.log (f n) + x * Real.log ((n : ℝ) - 1) ≤ Real.log (f (n + x)) ∧
      Real.log (f (n + x)) ≤ Real.log (f n) + x * Real.log n := by
  refine ⟨?_, ?_⟩
  · simpa [Function.comp_apply] using
      Real.BohrMollerup.f_add_nat_ge hf.log_convex hf.log_comp_feq hn hx
  · simpa [Function.comp_apply] using
      Real.BohrMollerup.f_add_nat_le hf.log_convex hf.log_comp_feq (by omega : n ≠ 0) hx hx'

Step 3: the Euler–Gauss limit¶

Now feed the product formula (3) into the sandwich (6). Taking logarithms of (3),

\log\big(f(n+x)\big)=\log\big(f(x)\big)+\sum_{m=0}^{n-1}\log(x+m),

(7)

and, exponentiating (6) after substitution and solving for $f(x)$ , one obtains for every $n$ the two-sided bound

\frac{(n-1)^{x}\,(n-1)!}{x(x+1)\cdots(x+n-1)}\;\le\;f(x)\;\le\;\frac{n^{x}\,n!}{x(x+1)\cdots(x+n)}\cdot\frac{n+x}{n}.

(8)

Because (8) holds for every $n$ , the left- and right-hand sides may use different indices. Sending $n\to\infty$ and using $\frac{n+x}{n}\to 1$ (equivalently $\log(n+1)-\log n\to 0$ ), the two sides converge to a common value, squeezing $f(x)$ to Gauss’s product limit

f(x)=\lim_{n\to\infty}\frac{n^{x}\,n!}{x(x+1)\cdots(x+n)} .

(9)

It is convenient to record this in logarithmic form. Setting

L_n(x):=x\log n+\log(n!)-\sum_{m=0}^{n}\log(x+m)

(10)

(so that $e^{L_n(x)}$ is exactly the fraction in (9)), the squeeze says $L_n(x)\to\log\big(f(x)\big)$ .

BohrMollerupFlow.lean

/-- **The Euler/Gauss limit formula for `f`.** Exponentiating and letting `n → ∞` in the sandwich of
step 2 squeezes the Gauss sequence
`logGammaSeq x n = x·log n + log n! − ∑_{m ≤ n} log (x + m)` (the logarithm of
`nˣ · n! / (x (x+1) ⋯ (x+n))`) to `log (f x)`. Because the limit does not depend on `f`, this is the
uniqueness engine of the theorem. -/
theorem GammaLike.logGammaSeq_tendsto (hf : GammaLike f) (hx : 0 < x) :
    Tendsto (Real.BohrMollerup.logGammaSeq x) atTop (𝓝 (Real.log (f x))) := by
  have h := Real.BohrMollerup.tendsto_logGammaSeq hf.log_convex hf.log_comp_feq hx
  simpa only [Function.comp_apply, hf.one, Real.log_one, sub_zero] using h

BohrMollerupFlow.lean

/-- **The explicit Gauss product.** Unwinding step 3, the value of any admissible `f` is Gauss's
product limit `f x = limₙ nˣ · n! / (x (x+1) ⋯ (x+n))`. -/
theorem GammaLike.gauss_product (hf : GammaLike f) (hx : 0 < x) :
    Tendsto (fun n : ℕ => (n : ℝ) ^ x * (n ! : ℝ) / ∏ j ∈ Finset.range (n + 1), (x + j))
      atTop (𝓝 (f x)) := by
  have h := Real.GammaSeq_tendsto_Gamma x
  rw [← hf.eq_Gamma hx] at h
  exact h

Here logGammaSeq x n is Mathlib’s name for $L_n(x)$ , and the squeeze itself (monotone secant slopes plus $\log(n+1)-\log n\to 0$ ) is provided by Mathlib’s Real.BohrMollerup.tendsto_logGammaSeq, which the Lean proof above specializes to our GammaLike hypotheses.

Step 4: uniqueness¶

The right-hand side of (9) makes no reference to $f$ : it is a fixed sequence built from $x$ and the integers. Hence its value is determined by $x$ alone. So if $f$ and $g$ both satisfy properties 1–3, then for every $x>0$

f(x)=\lim_{n\to\infty}\frac{n^{x}\,n!}{x(x+1)\cdots(x+n)}=g(x),

(11)

and the two functions coincide. In particular, since (as we check in Step 5) $\Gamma$ satisfies properties 1–3, and it too obeys $L_n(x)\to\log\Gamma(x)$ , the uniqueness of limits forces $\log f(x)=\log\Gamma(x)$ ; as $\log$ is injective on $(0,\infty)$ and both values are positive, $f(x)=\Gamma(x)$ for all $x>0$ .

BohrMollerupFlow.lean

/-- **Uniqueness (each admissible `f` equals `Γ`).** Both `f` and `Real.Gamma` make `logGammaSeq x`
converge — to `log (f x)` and to `log (Γ x)` respectively — so those logs are equal by uniqueness of
limits, and injectivity of `log` on the positive reals gives `f x = Γ x` for all `x > 0`. -/
theorem GammaLike.eq_Gamma (hf : GammaLike f) : EqOn f Real.Gamma (Ioi 0) := by
  intro x hx
  have hx0 : 0 < x := hx
  have hlog : Real.log (f x) = Real.log (Real.Gamma x) :=
    tendsto_nhds_unique (hf.logGammaSeq_tendsto hx0) (Real.BohrMollerup.tendsto_log_gamma hx0)
  exact Real.log_injOn_pos (hf.pos x hx0) (Real.Gamma_pos_of_pos hx0) hlog

BohrMollerupFlow.lean

/-- Any two functions with the three Bohr–Mollerup properties agree on `(0, ∞)`. -/
theorem GammaLike.unique (hf : GammaLike f) (hg : GammaLike g) : EqOn f g (Ioi 0) :=
  fun _ hx => (hf.eq_Gamma hx).trans (hg.eq_Gamma hx).symm

Step 5: existence — $\Gamma$ qualifies¶

Uniqueness would be vacuous without a function that actually meets all three conditions. The gamma function (1) does:

Normalization. $\Gamma(1)=\int_0^\infty e^{-t}\,\mathrm{d}t=1$ .
Functional equation. Integration by parts gives $\Gamma(x+1)=\big[-t^{x}e^{-t}\big]_0^\infty+x\int_0^\infty t^{x-1}e^{-t}\,\mathrm{d}t=x\,\Gamma(x)$ .
Log-convexity. Applying Hölder’s inequality to Euler’s integral shows $\log\Gamma$ is convex on $(0,\infty)$ .

Together with positivity of $\Gamma$ on $(0,\infty)$ , this establishes existence.

BohrMollerupFlow.lean

/-- **Existence.** `Real.Gamma` satisfies the three properties: it is positive
(`Real.Gamma_pos_of_pos`), obeys `Γ (x + 1) = x · Γ x` (`Real.Gamma_add_one`), is log-convex
(`Real.convexOn_log_Gamma`), and is normalized `Γ 1 = 1` (`Real.Gamma_one`). -/
theorem gammaLike_Gamma : GammaLike Real.Gamma where
  pos := fun _ hx => Real.Gamma_pos_of_pos hx
  functional_eq := fun _ hx => Real.Gamma_add_one hx.ne'
  log_convex := Real.convexOn_log_Gamma
  one := Real.Gamma_one

Conclusion¶

Steps 1–4 show that at most one positive function on $(0,\infty)$ can satisfy properties 1–3, and Step 5 shows $\Gamma$ is such a function. Therefore $\Gamma$ is the unique function with these properties — the Bohr–Mollerup theorem. The Lean statement bohr_mollerup in the first dropdown packages both halves: $\Gamma$ is GammaLike, and every GammaLike function equals $\Gamma$ on $(0,\infty)$ .

A pleasant by-product of the proof is the explicit Gauss product (9) for the gamma function, which fell out of the uniqueness argument without any extra work.

References¶

H. Bohr and J. Mollerup, Lærebog i matematisk Analyse, vol. III (1922) Bohr & Mollerup, 1922 — the original source.
E. Artin, The Gamma Function Artin, 1964 — the standard modern treatment, whose argument this note follows.
Bohr–Mollerup theorem on Wikipedia Wikipedia, 2025.

References¶

Bohr, H., & Mollerup, J. (1922). Lærebog i matematisk Analyse: Vol. III. Jul. Gjellerup.
Artin, E. (1964). The Gamma Function (M. Butler, Trans.). Holt, Rinehart.
Wikipedia. (2025). Bohr–Mollerup theorem. https://en.wikipedia.org/wiki/Bohr%5C%25E2%5C%2580%5C%2593Mollerup_theorem

The Bohr–Mollerup theorem

Step 1: the functional equation reproduces the factorials¶

Step 2: log-convexity sandwiches the values¶

Step 3: the Euler–Gauss limit¶

Step 4: uniqueness¶

Step 5: existence — Γ\GammaΓ qualifies¶

Conclusion¶

References¶

Step 5: existence — $\Gamma$ qualifies¶