Does convexity suffice in Bohr–Mollerup?

The Bohr–Mollerup theorem characterizes the gamma function as the unique positive function $f$ on $(0,\infty)$ with $f(1)=1$, $f(x+1)=x\,f(x)$, and $\log f$ convex (log-convex). A natural question:

Question. If we keep $f(1)=1$ and $f(x+1)=x\,f(x)$ but weaken “log-convex” to merely convex, is $\Gamma$ still the unique solution?

Answer: no. Convexity is not enough. Since a positive log-convex function is automatically convex — $f=\exp(\log f)$ and $\exp$ is convex increasing — replacing log-convexity by convexity is a strictly weaker hypothesis, so we should expect extra solutions, and indeed there are. This note exhibits an explicit one and proves it works.

1. Why the functional equation alone determines almost nothing¶

Fix any solution $f>0$ of $f(x+1)=x\,f(x)$ and compare it with $\Gamma$. Since $\Gamma(x+1)=x\,\Gamma(x)$ as well, the ratio $g:=f/\Gamma$ satisfies

So every solution has the form $f=\Gamma\cdot g$ with $g$ an arbitrary 1-periodic positive function; normalization forces only $g(1)=1$. The solution set is therefore infinite-dimensional. A shape hypothesis is what collapses it: log-convexity forces $g\equiv 1$ (a convex periodic function is constant), giving $f=\Gamma$. The question is whether plain convexity is a strong enough shape hypothesis. It is not.

/-- **The solution space of the functional equation.** For *any* `F` obeying `F (y+1) = y F y`, the
ratio `F / Γ` is `1`-periodic; equivalently every solution equals `Γ` times a `1`-periodic function.
So positivity + functional equation + `F 1 = 1` leave an infinite-dimensional family of solutions,
and only a *shape* hypothesis (log-convexity, or — the question here — convexity) can hope to
single out `Γ`. -/
theorem ratio_periodic {F : ℝ → ℝ} (hF : ∀ y, 0 < y → F (y + 1) = y * F y)
    {x : ℝ} (hx : 0 < x) : F (x + 1) / Gamma (x + 1) = F x / Gamma x := by
  have hx' : x ≠ 0 := hx.ne'
  have hg : Gamma x ≠ 0 := (Gamma_pos_of_pos hx).ne'
  rw [hF x hx, Gamma_add_one hx.ne']
  field_simp

2. The counterexample¶

For a small parameter $\varepsilon>0$ define the 1-periodic factor and the candidate function

Because $0\le 1-\cos 2\pi x\le 2$, we have $g_\varepsilon\ge 1>0$, and $g_\varepsilon$ has period 1 with $g_\varepsilon(n)=1$ at every integer (as $\cos 2\pi n=1$). Hence, exactly as in §1:

• Positivity: $f_\varepsilon(x)=\Gamma(x)\,g_\varepsilon(x)>0$ for $x>0$.

• Functional equation: $f_\varepsilon(x+1)=\Gamma(x+1)\,g_\varepsilon(x+1)=x\,\Gamma(x)\,g_\varepsilon(x)=x\,f_\varepsilon(x)$.

• Normalization: $f_\varepsilon(1)=\Gamma(1)\,g_\varepsilon(1)=1$.

These three are elementary and fully machine-checked.

/-- The `1`-periodic factor `1 + ε (1 - cos 2πx)`. It is `≥ 1`, so positive for `ε ≥ 0`; it equals
`1` at every integer; and it has period `1`. Multiplying `Γ` by it therefore keeps positivity, the
functional equation `f (x+1) = x f x`, and the normalization `f 1 = 1`. -/
noncomputable def perturb (ε x : ℝ) : ℝ := 1 + ε * (1 - Real.cos (2 * π * x))

/-- `perturb` has period `1`, since `cos` has period `2π`. -/
theorem perturb_periodic (ε x : ℝ) : perturb ε (x + 1) = perturb ε x := by
  have h : Real.cos (2 * π * (x + 1)) = Real.cos (2 * π * x) := by
    rw [show 2 * π * (x + 1) = 2 * π * x + 2 * π by ring]; exact Real.cos_add_two_pi _
  unfold perturb; rw [h]

/-- `perturb` is positive for `ε ≥ 0`, because `1 - cos ≥ 0`. -/
theorem perturb_pos (hε : 0 ≤ ε) (x : ℝ) : 0 < perturb ε x := by
  have h : 0 ≤ ε * (1 - Real.cos (2 * π * x)) :=
    mul_nonneg hε (by linarith [Real.cos_le_one (2 * π * x)])
  unfold perturb; linarith

/-- `perturb ε 1 = 1`, since `cos 2π = 1`. -/
theorem perturb_one (ε : ℝ) : perturb ε 1 = 1 := by
  have h : Real.cos (2 * π * 1) = 1 := by
    rw [show 2 * π * 1 = 2 * π by ring]; exact Real.cos_two_pi
  unfold perturb; rw [h]; ring

/-- The counterexample candidate `fᵥ(x) = Γ(x) · (1 + ε (1 - cos 2πx))`. -/
noncomputable def f (ε x : ℝ) : ℝ := Gamma x * perturb ε x

/-- `fᵥ` is positive on `(0, ∞)` for `ε ≥ 0` (a product of positives). -/
theorem f_pos (hε : 0 ≤ ε) {x : ℝ} (hx : 0 < x) : 0 < f ε x :=
  mul_pos (Gamma_pos_of_pos hx) (perturb_pos hε x)

/-- **Normalization** `fᵥ 1 = 1`, from `Γ 1 = 1` and `perturb ε 1 = 1`. -/
theorem f_one (ε : ℝ) : f ε 1 = 1 := by
  unfold f; rw [Gamma_one, perturb_one]; ring

/-- **The Gamma functional equation is preserved**: `fᵥ (x + 1) = x · fᵥ x` for `x > 0`, because
`Γ (x+1) = x Γ x` and `perturb` has period `1`. -/
theorem f_functional_eq {x : ℝ} (hx : 0 < x) : f ε (x + 1) = x * f ε x := by
  unfold f; rw [Gamma_add_one hx.ne', perturb_periodic]; ring

The convex counterexample is, to the eye, indistinguishable from $\Gamma$:

3. It differs from $\Gamma$, and it is not log-convex¶

At the half-integer, $\cos\pi=-1$, so

hence $f_\varepsilon\neq\Gamma$ whenever $\varepsilon>0$. Moreover $f_\varepsilon$ is not log-convex: if $\log\circ f_\varepsilon$ were convex on $(0,\infty)$, then the log-convex Bohr–Mollerup theorem (Mathlib’s Real.eq_Gamma_of_log_convex) — whose remaining hypotheses we verified in §2 — would force $f_\varepsilon=\Gamma$, contradicting (3). So $f_\varepsilon$ sits strictly below log-convexity. Once we show in §4 that it is nevertheless convex, the failure of the convex-hypothesis theorem is complete.

/-- The value at `x = 1/2`: `fᵥ(1/2) = Γ(1/2) · (1 + 2ε)`, since `cos π = -1`. -/
theorem f_half (ε : ℝ) : f ε (1 / 2) = Gamma (1 / 2) * (1 + 2 * ε) := by
  have hcos : Real.cos (2 * π * (1 / 2)) = -1 := by
    rw [show 2 * π * (1 / 2) = π by ring]; exact Real.cos_pi
  unfold f perturb; rw [hcos]; ring

/-- For `ε > 0`, `fᵥ` differs from `Γ`: they already disagree at `x = 1/2`, where
`fᵥ(1/2) = (1 + 2ε) Γ(1/2) > Γ(1/2)`. -/
theorem f_ne_Gamma (hε : 0 < ε) : ¬ Set.EqOn (f ε) Gamma (Ioi 0) := by
  intro hEq
  have h : f ε (1 / 2) = Gamma (1 / 2) := hEq (by norm_num : (1 / 2 : ℝ) ∈ Ioi (0 : ℝ))
  rw [f_half] at h
  have hg : 0 < Gamma (1 / 2 : ℝ) := Gamma_pos_of_pos (by norm_num)
  nlinarith [h, mul_pos hg hε]

/-- **`fᵥ` is not log-convex.** If `log ∘ fᵥ` were convex on `(0, ∞)`, then the log-convex
Bohr–Mollerup theorem `Real.eq_Gamma_of_log_convex` — whose other hypotheses (positivity, the
functional equation, `fᵥ 1 = 1`) we have verified — would force `fᵥ = Γ` on `(0, ∞)`, contradicting
`f_ne_Gamma`. So `fᵥ` lies strictly *below* log-convexity. Together with the convexity of `fᵥ`
(proved analytically in the note), this is exactly why convexity is too weak to characterize `Γ`. -/
theorem not_logConvex (hε : 0 < ε) : ¬ ConvexOn ℝ (Ioi 0) (log ∘ f ε) := by
  intro hconv
  have hEq : Set.EqOn (f ε) Gamma (Ioi 0) :=
    Real.eq_Gamma_of_log_convex hconv (fun {_} hy => f_functional_eq hy)
      (fun {_} hy => f_pos hε.le hy) (f_one ε)
  exact f_ne_Gamma hε hEq

4. It is convex (for small $\varepsilon$)¶

This is the crux. Write $u:=\log f_\varepsilon=\log\Gamma+v$ with $v:=\log g_\varepsilon$. Since $f_\varepsilon=e^{u}>0$,

Let $\psi:=(\log\Gamma)'$ (digamma) and $\psi':=(\log\Gamma)''$ (trigamma), so that $u'=\psi+v'$ and $u''=\psi'+v''$. We use two standard facts about $\Gamma$:

because $t\mapsto (x+t)^{-2}$ is positive and decreasing, and

Bounds on the perturbation. With $w:=\varepsilon(1-\cos 2\pi x)\in[0,2\varepsilon]$ we have $w'=2\pi\varepsilon\sin 2\pi x$ and $w''=4\pi^2\varepsilon\cos 2\pi x$, and since $g_\varepsilon=1+w\ge 1$,

Both $C_1,C_2=O(\varepsilon)$. Now split $(0,\infty)$ into two overlapping regions.

Region A: $0<x\le 1/C_2$. Here (5) gives $\psi'(x)\ge 1/x\ge C_2$, so $u''=\psi'+v''\ge C_2-C_2=0$. Together with $(u')^2\ge 0$ this yields $u''+(u')^2\ge 0$.

Region B: $x\ge X_1$, where $X_1$ is chosen (using (6)) so large that $\psi(x)\ge \sqrt{C_2}+C_1$ for all $x\ge X_1$. Then $u'=\psi+v'\ge\sqrt{C_2}+C_1-C_1=\sqrt{C_2}\ge 0$, so $(u')^2\ge C_2$, while $u''=\psi'+v''\ge 0-C_2=-C_2$ (as $\psi'>0$). Hence $u''+(u')^2\ge -C_2+C_2=0$.

Coverage. As $\varepsilon\to 0$ we have $C_1,C_2\to 0$, so $1/C_2\to\infty$ while $\sqrt{C_2}+C_1\to 0$ pushes $X_1$ down to the unique zero $x^\ast\approx 1.4616$ of $\psi$. Thus for all sufficiently small $\varepsilon>0$ we have $X_1\le 1/C_2$, the two regions cover $(0,\infty)$, and $u''+(u')^2\ge 0$ everywhere. By (4), $f_\varepsilon$ is convex. $\qquad\blacksquare$

For the concrete value $\varepsilon=\tfrac{1}{100}$ the constants already close: $C_2=4\pi^2(0.01)(1.01)\approx 0.399$, so $1/C_2\approx 2.51$, while $\sqrt{C_2}+C_1\approx 0.69$ is reached by $\psi$ already at $x\approx 2.49\le 2.51$. The next section confirms this numerically.

This entire argument is now machine-checked for $\varepsilon=\tfrac1{100}$. The linchpin is the trigamma lower bound, obtained from the trigamma recurrence $\psi'(x)=\psi'(x+1)+1/x^2$ (differentiate (6)), telescoping, and $\psi'\ge 0$: since $\psi'(x)=\sum_{k<n}\tfrac1{(x+k)^2}+\psi'(x+n)\ge\sum_{k<n}\tfrac1{(x+k)^2}\ge \tfrac1x-\tfrac1{x+n}$, letting $n\to\infty$ gives $\psi'(x)\ge 1/x$.

/-- **Trigamma lower bound** `(log Γ)''(x) ≥ 1/x` for `x > 0`. This is the one analytic fact the
note proves by hand; here it is machine-checked. From the digamma recurrence `ψ(x+1) = ψ(x) + 1/x`
we differentiate to get the trigamma recurrence `ψ'(x) = ψ'(x+1) + 1/x²`; telescoping and using
`ψ' ≥ 0` (convexity of `log Γ`) gives `ψ'(x) ≥ ∑_{k<n} 1/(x+k)² ≥ 1/x − 1/(x+n)`, and `n → ∞`
yields `ψ'(x) ≥ 1/x`. -/
theorem trig_ge {x : ℝ} (hx : 0 < x) : 1 / x ≤ trig x := by
  have key : ∀ n : ℕ, 1 / x - 1 / (x + n) ≤ trig x := by
    intro n
    have hsum_le : (∑ k ∈ Finset.range n, 1 / (x + (k:ℝ))^2) ≤ trig x := by
      rw [trig_telescope hx n]
      have : (0:ℝ) < x + n := by positivity
      linarith [trig_nonneg this]
    have hlb : 1 / x - 1 / (x + n) ≤ (∑ k ∈ Finset.range n, 1 / (x + (k:ℝ))^2) := by
      calc 1 / x - 1 / (x + n)
          = ∑ k ∈ Finset.range n, (1/(x+(k:ℝ)) - 1/(x+(k:ℝ)+1)) := (sum_tele n).symm
        _ ≤ ∑ k ∈ Finset.range n, 1 / (x + (k:ℝ))^2 := by
            apply Finset.sum_le_sum
            intro k _
            have hxk : (0:ℝ) < x + k := by positivity
            have hxk1 : (0:ℝ) < x + k + 1 := by positivity
            have e : 1/(x+(k:ℝ)) - 1/(x+(k:ℝ)+1) = 1/((x+k)*(x+k+1)) := by
              rw [div_sub_div _ _ (ne_of_gt hxk) (ne_of_gt hxk1), one_mul, mul_one]
              congr 1; ring
            rw [e]
            apply one_div_le_one_div_of_le (by positivity)
            nlinarith [hxk]
    linarith
  have hlim : Tendsto (fun n : ℕ => 1 / x - 1 / (x + n)) atTop (𝓝 (1 / x)) := by
    have hd : Tendsto (fun n : ℕ => x + (n:ℝ)) atTop atTop :=
      tendsto_atTop_add_const_left atTop x tendsto_natCast_atTop_atTop
    have h0 : Tendsto (fun n : ℕ => 1 / (x + (n:ℝ))) atTop (𝓝 0) :=
      (hd.inv_tendsto_atTop).congr (fun n => (one_div _).symm)
    simpa using (tendsto_const_nhds.sub h0)
  exact le_of_tendsto' hlim key

/-- **The counterexample is convex** for `ε = 1/100`. Writing `f = exp u` with `u = log Γ + log g`,
convexity is `u'' + (u')² ≥ 0`. On `(0, 5/2]` the trigamma bound gives `u'' ≥ 1/x − C₂ ≥ 0`
(Region A); on `[5/2, ∞)` the digamma value `ψ(5/2) = 8/3 − γ − 2 log 2` and monotonicity give
`(u')² ≥ C₂ ≥ −u''` (Region B). Here `C₁ = 2πε`, `C₂ = 4π²ε(1+ε)`. -/
theorem f_convex : ConvexOn ℝ (Ioi 0) (f (1/100)) := by
  have hε : (0:ℝ) ≤ 1/100 := by norm_num
  refine convexOn_of_hasDerivWithinAt2_nonneg (convex_Ioi 0) ?_
    (f' := Fst (1/100)) (f'' := Snd (1/100)) ?_ ?_ ?_
  · exact fun x hx => (hasDerivAt_f hε hx).continuousAt.continuousWithinAt
  · intro x hx
    rw [interior_Ioi] at hx
    exact (hasDerivAt_f hε hx).hasDerivWithinAt
  · intro x hx
    rw [interior_Ioi] at hx
    exact (hasDerivAt_Fst hε hx).hasDerivWithinAt
  · intro x hx
    rw [interior_Ioi] at hx
    unfold Snd
    exact mul_nonneg (f_pos hε hx).le (Q_nonneg hx)

5. Numerical confirmation¶

Sampling $f_\varepsilon''$ on a fine grid over $x\in(0,60]$ (second differences, step $2\times10^{-5}$) gives the minimum of $f_\varepsilon''$:

So $f_\varepsilon$ is convex for $\varepsilon\lesssim 0.02$ and loses convexity around $\varepsilon\approx 0.025$ — failing first in the tail, exactly where Region B is tightest. The headline value $\varepsilon=\tfrac1{100}$ sits comfortably inside the convex range ($\min f_\varepsilon''\approx 0.48$). The trigamma bound (5), $\psi'(x)\ge 1/x$, was also checked pointwise and holds with room to spare.

6. Why log-convexity? Fitting exponential data without wiggles¶

Step back to what we are really doing: interpolating the factorials, i.e. fitting the points $(n,(n-1)!)$. These grow exponentially, so the natural canvas for them is the semilogy plot, where the points become $(n,\log (n-1)!)$. By Stirling, $\log (n-1)! \approx n\log n - n$, so on that canvas they lie on a gently curving, almost straight line. A faithful interpolation should have no wiggles on either canvas — not on the ordinary linear plot, and not on this natural log plot.

These are two genuinely different requirements. The ripple $g_\varepsilon=1+\varepsilon(1-\cos 2\pi x)$ is a relative (multiplicative) modulation of a few percent: against factorial growth it is invisible on the linear axis but plainly visible on the log axis, where multiplicative structure becomes additive (Figure 1). And the two “no wiggle” demands are exactly the two notions of convexity:

• No wiggle on the linear plot $=$ $f$ convex $=$ $f'$ monotone. This forbids the derivative from ever decreasing (the obvious S-shaped wiggle). It is necessary, but not sufficient: $f_{0.01}$ is convex yet still carries the ripple, because $\Gamma$’s curvature is strong enough to keep $f'$ increasing while a small oscillation rides along.

• No wiggle on the log plot $=$ $f$ log-convex $=$ $(\log f)'=f'/f$ monotone. The relative growth rate is the natural quantity for a multiplicatively-defined object — the functional equation multiplies by $x$. Here $f_{0.01}$ fails: $(\log f_{0.01})'$ visibly turns over.

The two derivative tests side by side make this concrete: in $f'$ the convex $f_{0.01}$ stays monotone (only the non-convex $f_{0.20}$ dips), whereas in the log-derivative $f'/f$ the tiny $2\%$ ripple of $f_{0.01}$ is amplified to a clearly non-monotone wobble.

Because log-convex $\Rightarrow$ convex (for positive $f$, since $f=\exp(\log f)$ and $\exp$ is convex increasing), no wiggle on the log plot automatically implies no wiggle on the linear plot — it is the strictly stronger, and therefore decisive, requirement. That single demand — a smooth fit on the natural (log) canvas for exponential data — is exactly the log-convexity hypothesis, and by Bohr–Mollerup it pins down $\Gamma$ uniquely, whereas plain convexity does not.

7. What is proved where¶

Every hypothesis of the false theorem is machine-checked. For every $\varepsilon>0$, the bundled statement convex_hypothesis_insufficient collects that $f_\varepsilon$ is positive on $(0,\infty)$, satisfies $f_\varepsilon(x+1)=x\,f_\varepsilon(x)$ and $f_\varepsilon(1)=1$, is not equal to $\Gamma$, and is not log-convex.

/-- **Convexity is not sufficient (the machine-checked core).** For every `ε > 0`, `fᵥ` is a
positive solution of the Gamma functional equation with `fᵥ 1 = 1` that is **not** equal to `Γ` and
is **not** log-convex. The note proves analytically (and confirms numerically) that for small `ε`
(e.g. `ε = 1/100`) it is moreover **convex** — so, unlike log-convexity, plain convexity does not
determine `Γ`. -/
theorem convex_hypothesis_insufficient (hε : 0 < ε) :
    (∀ x, 0 < x → 0 < f ε x) ∧
      (∀ x, 0 < x → f ε (x + 1) = x * f ε x) ∧
      f ε 1 = 1 ∧
      ¬ Set.EqOn (f ε) Gamma (Ioi 0) ∧
      ¬ ConvexOn ℝ (Ioi 0) (log ∘ f ε) :=
  ⟨fun _ hx => f_pos hε.le hx, fun _ hx => f_functional_eq hx, f_one ε,
    f_ne_Gamma hε, not_logConvex hε⟩

The crux — that $f_\varepsilon$ is also convex — is now machine-checked for the headline value $\varepsilon=\tfrac1{100}$ (f_convex, §4). Because current Mathlib has no di-/tri-gamma theory, the Lean file builds it from scratch: it establishes the $C^2$-smoothness of $\log\Gamma$ (from the analyticity of the complex $\Gamma$), the digamma recurrence $\psi(x+1)=\psi(x)+1/x$, and the trigamma lower bound $(\log\Gamma)''(x)\ge 1/x$; convexity then follows from the $C^2$ criterion, using the digamma value $\psi(\tfrac12)=-\gamma-2\log2$ (from Mathlib’s $\Gamma'(\tfrac12)$) and monotonicity of $\psi$ for the Region-B hand-off at $x=\tfrac52$. The single non-elementary numeric input is a sharpened bound $\gamma<\tfrac{29}{50}$ on the Euler–Mascheroni constant, obtained from Mathlib’s $\gamma<\text{harmonic}(256)-\log 256$ and its precise bounds on $\log 2$.

The complete counterexample is bundled in convexity_hypotheses_hold: for $\varepsilon=\tfrac1{100}$, $f_\varepsilon$ is positive, satisfies the functional equation and $f_\varepsilon(1)=1$, is convex, is not equal to $\Gamma$, and is not log-convex — so convexity, normalization and the functional equation together do not characterize $\Gamma$.

/-- **The counterexample satisfies every hypothesis of the (false) "convex Bohr–Mollerup"
theorem, yet is not `Γ`.** For `ε = 1/100`, `fᵥ` is positive on `(0, ∞)`, obeys the Gamma
functional equation `fᵥ(x+1) = x·fᵥ(x)`, is normalized `fᵥ 1 = 1`, is **convex** on `(0, ∞)`,
and is **not** log-convex — hence `fᵥ ≠ Γ`. So replacing "log-convex" by "convex" in
Bohr–Mollerup is false: convexity, normalization and the functional equation do **not** pin
down `Γ`. Every conjunct here is machine-checked (including the previously hand-proved
convexity). -/
theorem convexity_hypotheses_hold :
    (∀ x, 0 < x → 0 < f (1/100) x) ∧
      (∀ x, 0 < x → f (1/100) (x + 1) = x * f (1/100) x) ∧
      f (1/100) 1 = 1 ∧
      ConvexOn ℝ (Ioi 0) (f (1/100)) ∧
      ¬ Set.EqOn (f (1/100)) Gamma (Ioi 0) ∧
      ¬ ConvexOn ℝ (Ioi 0) (log ∘ f (1/100)) :=
  ⟨fun _ hx => f_pos (by norm_num) hx, fun _ hx => f_functional_eq hx, f_one _,
    f_convex, f_ne_Gamma (by norm_num), not_logConvex (by norm_num)⟩

Conclusion¶

Convexity does not replace log-convexity in the Bohr–Mollerup theorem: for every small $\varepsilon>0$ the function $f_\varepsilon(x)=\Gamma(x)\bigl(1+\varepsilon(1-\cos 2\pi x)\bigr)$ is a convex, positive solution of $f(x+1)=x\,f(x)$ with $f(1)=1$ that is different from $\Gamma$. The log-convexity hypothesis of the original theorem is therefore essential — it is exactly strong enough to eliminate the periodic perturbations that plain convexity tolerates. For $\varepsilon=\tfrac1{100}$ this is now verified end-to-end in Lean, convexity included.

References¶

• The companion note The Bohr–Mollerup theorem proves the log-convex version.

• E. Artin, The Gamma Function Artin, 1964, discusses the role of log-convexity.

• Bohr–Mollerup theorem on Wikipedia Wikipedia, 2025.