convexOn_Gamma — Mathlib

English

The reciprocal of the Gamma function is differentiable everywhere on ℂ.

Русский

Обратная к Гамма-функции дифференцируема на всей плоскости ℂ.

LaTeX

$$$$ \text{Differentiable } \mathbb{C} \to (\Gamma(\cdot))^{-1}. $$$$

Lean4

theorem convexOn_Gamma : ConvexOn ℝ (Ioi 0) Gamma :=
  by
  refine
    ((convexOn_exp.subset (subset_univ _) ?_).comp convexOn_log_Gamma (exp_monotone.monotoneOn _)).congr fun x hx =>
      exp_log (Gamma_pos_of_pos hx)
  rw [convex_iff_isPreconnected]
  refine isPreconnected_Ioi.image _ fun x hx => ContinuousAt.continuousWithinAt ?_
  refine (differentiableAt_Gamma fun m => ?_).continuousAt.log (Gamma_pos_of_pos hx).ne'
  exact (neg_lt_iff_pos_add.mpr (add_pos_of_pos_of_nonneg (mem_Ioi.mp hx) (Nat.cast_nonneg m))).ne'

Похожие утверждения