Theorem 8.18 — functional equation and log-convexity of $\Gamma$

Proved

Rudin.ch08_gamma_functional_equation

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

analysisspecial-functions

For $x > 0$ , $\Gamma(x+1) = x\Gamma(x)$ ; $\Gamma(n+1) = n!$ for nonnegative integers $n$ ; and $\log \Gamma$ is convex on $(0,\infty)$ .

Preamble

import Mathlib
import Definitions.Def_Rudin_ch08_fourier

open Filter Topology

Formal statement

namespace Rudin

/-- Rudin, Theorem 8.18: the Gamma function satisfies `Γ(x+1) = x Γ(x)` for `x > 0`,
`Γ(n+1) = n!` for nonnegative integers `n`, and `log Γ` is convex on `(0, ∞)`. -/
theorem ch08_gamma_functional_equation :
    (∀ x : ℝ, 0 < x → Real.Gamma (x + 1) = x * Real.Gamma x) ∧
    (∀ n : ℕ, Real.Gamma (n + 1) = n.factorial) ∧
    ConvexOn ℝ (Set.Ioi (0 : ℝ)) (fun x => Real.log (Real.Gamma x)) := by sorry

end Rudin

Source

Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 8, pp. 192-193, Definition 8.17 and Theorem 8.18

Read-back

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

Three unconditional assertions about the real Gamma function $\Gamma$ , combined into one statement:

For every real $x > 0$ : $\Gamma(x+1) = x\,\Gamma(x)$ .
For every natural number $n$ : $\Gamma(n+1) = n!$ (the factorial cast into $\mathbb{R}$ ; the case $n=0$ gives $\Gamma(1)=1$ ).
The function $x \mapsto \log \Gamma(x)$ is convex on the open half-line $(0,\infty)$ : for $x,y$ in it and weights $s,t \ge 0$ with $s+t=1$ , $\log\Gamma(sx+ty) \le s\log\Gamma(x) + t\log\Gamma(y)$ .

Item 1 is restricted to positive arguments; nothing is claimed for $x \le 0$ , where $\Gamma$ is still a total function. Item 3 uses the real logarithm, which returns $0$ on non-positive arguments, and includes implicitly that the domain $(0,\infty)$ is convex.

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.18 — functional equation and log-convexity of Γ\GammaΓ

Theorem 8.18 — functional equation and log-convexity of $\Gamma$