English
If a function f is log-convex on (0, ∞), nonnegative on (0, ∞), satisfies f(1) = 1 and the recurrence f(y+1) = y f(y) for y > 0, then f coincides with the Gamma function on (0, ∞).
Русский
Если функция f логарифмически выпукла на (0, ∞), неотрицательна на (0, ∞), удовлетворяет f(1)=1 и тождественный переход f(y+1)=y f(y) для y>0, то f совпадает с функцией Гамма на (0, ∞).
LaTeX
$$$ \text{If } f: \mathbb{R}_{>0} \to \mathbb{R} \text{ is log-convex on } (0,\infty),\; f(y+1)=y f(y),\; f(1)=1,\; \text{and } f(y)>0, \text{ then } f(x)=\Gamma(x) \text{ for } x>0.$$$
Lean4
/-- The **Bohr-Mollerup theorem**: the Gamma function is the *unique* log-convex, positive-valued
function on the positive reals which satisfies `f 1 = 1` and `f (x + 1) = x * f x` for all `x`. -/
theorem eq_Gamma_of_log_convex {f : ℝ → ℝ} (hf_conv : ConvexOn ℝ (Ioi 0) (log ∘ f))
(hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = y * f y) (hf_pos : ∀ {y : ℝ}, 0 < y → 0 < f y) (hf_one : f 1 = 1) :
EqOn f Gamma (Ioi (0 : ℝ)) :=
by
suffices EqOn (log ∘ f) (log ∘ Gamma) (Ioi (0 : ℝ)) from fun x hx ↦
log_injOn_pos (hf_pos hx) (Gamma_pos_of_pos hx) (this hx)
intro x hx
have e1 := BohrMollerup.tendsto_logGammaSeq hf_conv ?_ hx
· rw [Function.comp_apply (f := log) (g := f) (x := 1), hf_one, log_one, sub_zero] at e1
exact tendsto_nhds_unique e1 (BohrMollerup.tendsto_log_gamma hx)
· intro y hy
rw [Function.comp_apply, Function.comp_apply, hf_feq hy, log_mul hy.ne' (hf_pos hy).ne']
ring
