English
The reciprocal map s ↦ Γℝ(s)^{-1} is complex-differentiable.
Русский
Обратная к функции Γℝ по комплексной переменной дифференцируема.
LaTeX
$$$$ s \mapsto \Gamma_{\mathbb{R}}(s)^{-1} \text{ is differentiable on } \mathbb{C}. $$$$
Lean4
theorem differentiable_Gammaℝ_inv : Differentiable ℂ (fun s ↦ (Gammaℝ s)⁻¹) :=
by
conv => enter [2, s]; rw [Gammaℝ, mul_inv]
refine Differentiable.mul (fun s ↦ .inv ?_ (by simp [pi_ne_zero])) ?_
· refine ((differentiableAt_id.neg.div_const (2 : ℂ)).const_cpow ?_)
exact Or.inl (ofReal_ne_zero.mpr pi_ne_zero)
· exact differentiable_one_div_Gamma.comp (differentiable_id.div_const _)