English
The reciprocal of the Gamma function is differentiable everywhere on ℂ.
Русский
Обратная к Гамма-функции является дифференцируемой на всей области ℂ.
LaTeX
$$$$ \text{Differentiable } \mathbb{C} \to (\Gamma(\cdot))^{-1}. $$$$
Lean4
/-- The reciprocal of the Gamma function is differentiable everywhere
(including the points where Gamma itself is not). -/
theorem differentiable_one_div_Gamma : Differentiable ℂ fun s : ℂ => (Gamma s)⁻¹ := fun s ↦
by
rcases exists_nat_gt (-s.re) with ⟨n, hs⟩
induction n generalizing s with
| zero =>
rw [Nat.cast_zero, neg_lt_zero] at hs
suffices ∀ m : ℕ, s ≠ -↑m from (differentiableAt_Gamma _ this).inv (Gamma_ne_zero this)
rintro m rfl
apply hs.not_ge
simp
| succ n ihn =>
rw [funext one_div_Gamma_eq_self_mul_one_div_Gamma_add_one]
specialize ihn (s + 1) (by rwa [add_re, one_re, neg_add', sub_lt_iff_lt_add, ← Nat.cast_succ])
exact differentiableAt_id.mul (ihn.comp s (f := fun s => s + 1) <| differentiableAt_id.add_const (1 : ℂ))
