English
Γ(3/2) < 1.
Русский
Γ(3/2) < 1.
LaTeX
$$$ \Gamma\left(\tfrac{3}{2}\right) < 1 $$$
Lean4
theorem Gamma_three_div_two_lt_one : Gamma (3 / 2) < 1 := by
-- This can also be proved using the closed-form evaluation of `Gamma (1 / 2)` in
-- `Mathlib/Analysis/SpecialFunctions/Gaussian.lean`, but we give a self-contained proof using
-- log-convexity to avoid unnecessary imports.
have A : (0 : ℝ) < 3 / 2 := by simp
have :=
BohrMollerup.f_add_nat_le convexOn_log_Gamma (fun {y} hy => ?_) two_ne_zero one_half_pos
(by norm_num : 1 / 2 ≤ (1 : ℝ))
swap
·
rw [Function.comp_apply, Gamma_add_one hy.ne', log_mul hy.ne' (Gamma_pos_of_pos hy).ne', add_comm,
Function.comp_apply]
rw [Function.comp_apply, Function.comp_apply, Nat.cast_two, Gamma_two, log_one, zero_add,
(by norm_num : (2 : ℝ) + 1 / 2 = 3 / 2 + 1), Gamma_add_one A.ne', log_mul A.ne' (Gamma_pos_of_pos A).ne', ←
le_sub_iff_add_le', log_le_iff_le_exp (Gamma_pos_of_pos A)] at this
refine this.trans_lt (exp_lt_one_iff.mpr ?_)
rw [mul_comm, ← mul_div_assoc, div_sub' two_ne_zero]
refine div_neg_of_neg_of_pos ?_ two_pos
rw [sub_neg, mul_one, ← Nat.cast_two, ← log_pow, ← exp_lt_exp, Nat.cast_two, exp_log two_pos, exp_log] <;> norm_num
